HSF(C): A Software Verifier based on Horn Clauses

Overview

HSF 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.

The tool should be run as follows: ./qarmc.sh file.c. The working directory should be the directory where HSF's files are located.

People contributing to the project:

• Sergey Grebenshchikov
• Ashutosh Gupta
• Nuno P. Lopes
• Corneliu Popeea
• Andrey Rybalchenko

Last modified: 25-Jan-2012.