Note: This is an archvied version of our old webpage. Some links might be broken. The current one can be found here.
I7 Logo
Chair for Foundations of Software Reliability and Theoretical Computer Science
Informatik Logo TUM Logo
HSF(C): A Software Verifier based on Horn Clauses


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.

Download HSF(C) (x86-32 Linux)

The tool should be run as follows: ./ 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.