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.
展开▼
