Advertisement

Triggerless Happy

Intermediate Verification with a First-Order Prover
  • YuTing ChenEmail author
  • Carlo A. Furia
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10510)

Abstract

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.

Notes

Acknowledgments

We thank Evgenii Kotelnikov for helping us understand the latest features of Vampire’s support for FOOL.

References

  1. 1.
    Ameri, M., Furia, C.A.: Why just Boogie? Translating between intermediate verification. In: Ábrahám, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 79–95. Springer, Cham (2016). doi: 10.1007/978-3-319-33693-0_6 CrossRefGoogle Scholar
  2. 2.
    Amin, N., Leino, K.R.M., Rompf, T.: Computing with an SMT solver. In: Seidl, M., Tillmann, N. (eds.) TAP 2014. LNCS, vol. 8570, pp. 20–35. Springer, Cham (2014). doi: 10.1007/978-3-319-09099-3_2 Google Scholar
  3. 3.
    Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011). doi: 10.1007/978-3-642-22110-1_14 CrossRefGoogle Scholar
  4. 4.
    Böhme, S., Leino, K.R.M., Wolff, B.: HOL-Boogie — an interactive prover for the boogie program-verifier. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 150–166. Springer, Heidelberg (2008). doi: 10.1007/978-3-540-71067-7_15 CrossRefGoogle Scholar
  5. 5.
    Böhme, S., Moskal, M.: Heaps and data structures: a challenge for automated provers. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 177–191. Springer, Heidelberg (2011). doi: 10.1007/978-3-642-22438-6_15 CrossRefGoogle Scholar
  6. 6.
    Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). doi: 10.1007/978-3-540-78800-3_24 CrossRefGoogle Scholar
  7. 7.
    Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52, 365–473 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Dross, C., Conchon, S., Kanig, J., Paskevich, A.: Reasoning with triggers. In: SMT. EPiC Series, pp. 22–31. EasyChair (2012)Google Scholar
  9. 9.
    Flanagan, C., Saxe, J.B.: Avoiding exponential explosion: generating compact verification conditions. In: POPL, pp. 193–205. ACM (2001)Google Scholar
  10. 10.
    Furia, C.A., Meyer, B., Velder, S.: Loop invariants: analysis, classification, and examples. ACM Comp. Sur. 46(3) (2014)Google Scholar
  11. 11.
    Gries, D.: The Science of Programming. Springer, New York (1981)CrossRefzbMATHGoogle Scholar
  12. 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. 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. 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
  15. 15.
    Kovács, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1–35. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-39799-8_1 CrossRefGoogle Scholar
  16. 16.
    Leino, K.R.M.: Efficient weakest preconditions. Inf. Process. Lett. 93(6), 281–288 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Leino, K.R.M., Monahan, R.: Reasoning about comprehensions with first-order SMT solvers. In: SAC, pp. 615–622. ACM (2009)Google Scholar
  18. 18.
    Leino, K.R.M., Pit-Claudel, C.: Trigger selection strategies to stabilize program verifiers. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 361–381. Springer, Cham (2016). doi: 10.1007/978-3-319-41528-4_20 Google Scholar
  19. 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. 20.
    Nelson, C.G.: Techniques for program verification. Ph.D. thesis, Xerox PARC (1981). CSL-81-10Google Scholar
  21. 21.
    Polikarpova, N., Furia, C.A., West, S.: To run what no one has run before: executing an intermediate verification language. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 251–268. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-40787-1_15 CrossRefGoogle Scholar
  22. 22.
    Rümmer, P.: E-matching with free variables. In: Bjørner, N., Voronkov, A. (eds.) LPAR 2012. LNCS, vol. 7180, pp. 359–374. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-28717-6_28 CrossRefGoogle Scholar
  23. 23.
    Sutcliffe, G.: The TPTP problem library and associated infrastructure. J. Autom. Reason. 43(4), 337–362 (2009)CrossRefzbMATHGoogle Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.Chalmers University of TechnologyGothenburgSweden

Personalised recommendations