Induction for SMT Solvers

Satisfiability modulo theory solvers are increasingly being used to solve quantified formulas over structures such as integers and term algebras. Quantifier instantiation combined with ground decision procedure alone is insufficient to prove many formulas of interest in such cases. We present a set of techniques that introduce inductive reasoning into SMT solving algorithms that is sound with respect to the interpretation of structures in SMT-LIB standard. The techniques include inductive strengthening of conjecture to be proven, as well as facility to automatically discover subgoals during an inductive proof, where subgoals themselves can be proven using induction. The techniques have been implemented in CVC4. Our experiments show that the developed techniques have good performance and coverage of a range of inductive reasoning problems. Our experiments also show the impact of different representations of natural numbers and quantifier instantiation techniques on the performance of inductive reasoning. Our solution is freely available in the CVC4 development repository. In addition its overall effectiveness, it has an advantage of accepting SMT-LIB input and being integrated with other SMT solving techniques of CVC4.


Editor(s):
Dsouza, D
Lal, A
Larsen, Kg
Published in:
Verification, Model Checking, And Abstract Interpretation (Vmcai 2015), 8931, 80-98
Presented at:
16th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), Mumbai, INDIA, JAN 12-14, 2015
Year:
2015
Publisher:
Berlin, Springer-Verlag Berlin
ISSN:
0302-9743
ISBN:
978-3-662-46081-8
978-3-662-46080-1
Laboratories:




 Record created 2015-09-28, last modified 2018-09-13


Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)