de.mpg.escidoc.pubman.appbase.FacesBean
English
 
Help Guide Disclaimer Contact us Login
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Conference Paper

Incremental Instance Generation in Local Reasoning

MPS-Authors
http://pubman.mpdl.mpg.de/cone/persons/resource/persons44687

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

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

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
Abstract
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.