Incremental Instance Generation in Local Reasoning
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.
- 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
- 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