Incremental Instance Generation in Local Reasoning

  • Swen Jacobs
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5643)


Many verification approaches use SMT solvers in some form, and are limited by their incomplete handling of quantified formulas. Local reasoning allows to handle SMT problems involving a certain class of universally quantified formulas in a complete way by instantiation to a finite set of ground formulas. We present a method to generate these instances incrementally, in order to provide a more efficient way of solving these satisfiability problems. The incremental instantiation is guided semantically, inspired by the instance generation approach to first-order theorem proving. Our method is sound and complete, and terminates on both satisfiable and unsatisfiable input after generating a subset of the instances needed in standard local reasoning. Experimental results show that for a large class of examples the incremental approach is substantially more efficient than eager generation of all instances.


  1. 1.
    Bradley, A.R., Manna, Z., Sipma, H.B.: What’s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 427–442. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  2. 2.
    de 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)CrossRefGoogle Scholar
  3. 3.
    Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. Journal of the ACM 52(3), 365–473 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Ganzinger, H.: Relating semantic and proof-theoretic concepts for polynomial time decidability of uniform word problems. In: 16th IEEE Symposium on Logic in Computer Science, pp. 81–92. IEEE Computer Society Press, New York (2001)Google Scholar
  5. 5.
    Ganzinger, H., Korovin, K.: Theory instantiation. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS, vol. 4246, pp. 497–511. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  6. 6.
    Ge, Y., Barrett, C., Tinelli, C.: Solving Quantified Verification Conditions Using Satisfiability Modulo Theories. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 167–182. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  7. 7.
    Givan, R., McAllester, D.: Polynomial-time computation via local inference relations. ACM Transactions on Computational Logic 3(4), 521–541 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Ihlemann, C., Jacobs, S., Sofronie-Stokkermans, V.: On local reasoning in verification. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 265–281. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  9. 9.
    Jacobs, S., Sofronie-Stokkermans, V.: Applications of Hierarchical Reasoning in the Verification of Complex Systems. In: Fourth Workshop on Pragmatics of Decision Procedures in Automated Reasoning. ENTCS, vol. 174(8), pp. 39–54. Elsevier, Amsterdam (2007)Google Scholar
  10. 10.
    McPeak, S., Necula, G.C.: Data structure specifications via local equality axioms. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 476–490. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  11. 11.
    Nieuwenhuis, R., Oliveras, A., Rodriguez-Carbonell, E., Rubio, A.: Challenges in Satisfiability Modulo Theories. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 2–18. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  12. 12.
    Sofronie-Stokkermans, V.: Hierarchic reasoning in local theory extensions. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 219–234. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  13. 13.
    Veanes, M., Bjørner, N., Raschke, A.: An SMT Approach to Bounded Reachability Analysis of Model Programs. In: Suzuki, K., Higashino, T., Yasumoto, K., El-Fakih, K. (eds.) FORTE 2008. LNCS, vol. 5048, pp. 53–68. Springer, Heidelberg (2008)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Swen Jacobs
    • 1
  1. 1.Max-Planck-Institut für InformatikSaarbrückenGermany

Personalised recommendations