HSF(C): A Software Verifier Based on Horn Clauses (Competition Contribution)
Sergey Grebenshchikov, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea, Andrey Rybalchenko · Tools and Algorithms for Construction and Analysis of Systems · 2012
HSF(C) is a tool that automates verification of safety and liveness properties for C programs. This paper describes the verification approach taken by HSF(C) and provides instructions on how to install and use the tool.