Solving Horn clauses for verification and synthesis

Given our experience in designing and manually implementing software verifiers for different classes of properties and applicable to different programming languages, we introduce in [1] an algorithm that is able to synthesize automatically a large class of software verifiers. [1] takes a number of proof rules used in seminal verification papers (e.g., transition invariants, procedure summarization, Owicki-Gries reasoning, rely-guarantee reasoning for safety and for termination), uniformly represents them as Horn clauses and synthesises automatically verifiers. Our experience with one of these automatically generated verifiers is presented in [2], a verifier that was awarded a bronze medal in competition with manually-implemented (automated) verifiers competing in SV-COMP held during the TACAS conference in 2012.

  1. PLDI 2012 Synthesizing software verifiers from proof rules (pdf) (slides)
  2. TACAS 2012 HSF(C): A software verifier based on Horn clauses - (Competition Contribution) (pdf) (slides) (project webpage)
  3. CAV 2013 Solving existentially quantified Horn clauses (pdf) (slides)
  4. POPL 2014 A constraint-based approach to solving games on infinite graphs (pdf)

Download

The x86-32 binaries for our competition candidate HSF(C) can be downloaded from the SV-COMP webpage (here). The HSF archive contains three binaries and a script: 1) a frontend for C programs (main.native); 2) a Horn-clause generator (summ2q); 3) a model checker (qarmc) and 4) a script that runs the previous binaries with appropriate parameters (qarmc.sh). You could use a more recent version of the qarmc binary from

Thanks for reporting bugs and feedback to Hossein Hojjat, Alexander Malkis, Omar Inverso.

This project is joint work with Tewodros Beyene, Swarat Chaudhuri, Sergey Grebenshchikov, Ashutosh Gupta, Nuno Lopes and Andrey Rybalchenko.