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