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

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

 

Abstract:

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.

 

Published:

S. Grebenshchikov, A. Gupta, N. P. Lopes, C. Popeea, A. Rybalchenko. HSF(C): A Software Verifier based on Horn Clauses (Competition Contribution). In Proc. of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Mar. 2012.

 

Download:

 

Bibtex:

@inproceedings{hsfc-tacas12,
  title =	{{HSF}(C): A Software Verifier based on Horn Clauses (Competition Contribution)},
  author =	{Sergey Grebenshchikov and Ashutosh Gupta and Nuno P. Lopes and Corneliu Popeea and Andrey Rybalchenko},
  booktitle =	{Proc. of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
  doi =		{10.1007/978-3-642-28756-5_46},
  month =	mar,
  year =	2012
}

 

Copyright notice:

The final publication is available at link.springer.com.

 

<-- Return