SMT solvers have become de rigueur in deductive verification to automatically prove the validity of verification conditions. While these solvers provide an effective support for theories—such as arithmetic—that feature strongly in program verification, they tend to be more limited in dealing with first-order quantification, for which they have to rely on special annotations—known as triggers—to guide the instantiation of quantifiers. Writing effective triggers is necessary to achieve satisfactory performance with SMT solvers, but remains a tricky endeavor—beyond the purview of non-highly trained experts.
In this paper, we experiment with the idea of using first-order provers instead of SMT solvers to prove the validity of verification conditions. First-order provers offer a native support for unrestricted quantification, but have been traditionally limited in theory reasoning. By leveraging some recent extensions to narrow this gap in the Vampire first-order prover, we describe a first-order encoding of verification conditions of programs written in the Boogie intermediate verification language. Experiments with a prototype implementation on a variety of Boogie programs suggest that first-order provers can help achieve more flexible and robust performance in program verification, while avoiding the pitfalls of having to manually guide instantiations by means of triggers.
We thank Evgenii Kotelnikov for helping us understand the latest features of Vampire’s support for FOOL.
- 8.Dross, C., Conchon, S., Kanig, J., Paskevich, A.: Reasoning with triggers. In: SMT. EPiC Series, pp. 22–31. EasyChair (2012)Google Scholar
- 9.Flanagan, C., Saxe, J.B.: Avoiding exponential explosion: generating compact verification conditions. In: POPL, pp. 193–205. ACM (2001)Google Scholar
- 10.Furia, C.A., Meyer, B., Velder, S.: Loop invariants: analysis, classification, and examples. ACM Comp. Sur. 46(3) (2014)Google Scholar
- 12.Kaliszyk, C., Sutcliffe, G., Rabe, F.: TH1: the TPTP typed higher-order form with rank-1 polymorphism. In: PAAR at IJCAR. CEUR Workshop Proceedings, vol. 1635, pp. 41–55. CEUR-WS.org (2016)
- 13.Kotelnikov, E., Kovács, L., Reger, G., Voronkov, A.: The Vampire and the FOOL. In: SIGPLAN CPP, pp. 37–48. ACM (2016)Google Scholar
- 14.Kotelnikov, E., Kovács, L., Suda, M., Voronkov, A.: A clausal normal form translation for FOOL. In: GCAI. EPiC, vol. 41, pp. 53–71. EasyChair (2016)Google Scholar
- 17.Leino, K.R.M., Monahan, R.: Reasoning about comprehensions with first-order SMT solvers. In: SAC, pp. 615–622. ACM (2009)Google Scholar
- 19.Liew, D., Cadar, C., Donaldson, A.F.: Symbooglix: a symbolic execution engine for Boogie programs. In: ICST, pp. 45–56. IEEE Computer Society (2016)Google Scholar
- 20.Nelson, C.G.: Techniques for program verification. Ph.D. thesis, Xerox PARC (1981). CSL-81-10Google Scholar