salle A. Turing CE4
28 mai 2015 - 14h00
Using CVC4 for Proofs by Induction in SMT
par Andrew Reynolds de EPFL Lausanne
Abstract: Satisfiability modulo theory solvers are increasingly being used to solve quantified formulas over structures such as integers and term algebras. This talk presents a set of techniques for integrating inductive reasoning within 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. We discuss an implementation of these techniques in the SMT solver CVC4. We present an evaluation focusing on the impact of different encodings of inductive problems in the SMT-LIB standard.
