User Manual Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse




Conference Paper

Incremental Instance Generation in Local Reasoning


Jacobs,  Swen
Automation of Logic, MPI for Informatics, Max Planck Society;

There are no locators available
Fulltext (public)
There are no public fulltexts available
Supplementary Material (public)
There is no public supplementary material available

Jacobs, S. (2009). Incremental Instance Generation in Local Reasoning. In A. Bouajjani, & O. Maler (Eds.), Computer Aided Verification (pp. 368-382). Berlin: Springer.

Cite as: http://hdl.handle.net/11858/00-001M-0000-000F-1A5C-D
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.