HSF(C): A Software Verifier based on Horn Clauses. SF is a framework that automates verification of programs. HSF(C) is the instantiation of HSF for verification of C programs. HSF(C) is based on predicate abstraction and refinement following the CEGAR paradigm. There are a number of successful tools including SLAM, Blast, ARMC and CPAChecker that are also based on abstraction refinement. By using abstraction refinement, HSF(C) finds auxiliary assertions required for proving software properties automatically.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element