Model-Based Reasoning About Quantified Formulas in SMT
Event details
| Date | 18.09.2013 |
| Hour | 14:00 › 15:00 |
| Speaker | Andrew Reynolds |
| Location | |
| Category | Conferences - Seminars |
Satisfiability Modulo Theories (SMT) solvers have emerged as powerful tools in formal methods applications in recent years, due in part to advances in decision procedures for ground theories for arithmetic, arrays, bit-vectors and recursive datatypes. An ongoing challenge in the SMT community has been how to handle the presence of universally quantified formulas. Typically, when such formulas are present, a solver will either answer "unsatisfiable" if the solver is able to find a proof, or otherwise will answer "unknown" after some predetermined amount of effort. For many applications, however, it is often critical to know when such formulas are guaranteed to be satisfiable, and moreover to have a model that demonstrates the satisfiability. For instance, in verification applications, a model may correspond to a concrete counterexample for safety property in question.
This talk examines various model-based approaches for reasoning about quantified formulas in SMT. One approach, finite model finding, can establish the satisfiability of a quantified formula whose domain is finite by exhaustively testing all of its ground instances. While this may not be practical for quantified formulas with large domain sizes, various techniques can minimize domain sizes and identify when sets of instances are not relevant. Similar approaches may be applied to further domains and applications, including the case of quantification over integer variables where finite bounds can be inferred. Experimental results are given for an implementation of a finite model finding capability in the SMT solver CVC4.
This talk examines various model-based approaches for reasoning about quantified formulas in SMT. One approach, finite model finding, can establish the satisfiability of a quantified formula whose domain is finite by exhaustively testing all of its ground instances. While this may not be practical for quantified formulas with large domain sizes, various techniques can minimize domain sizes and identify when sets of instances are not relevant. Similar approaches may be applied to further domains and applications, including the case of quantification over integer variables where finite bounds can be inferred. Experimental results are given for an implementation of a finite model finding capability in the SMT solver CVC4.
Practical information
- Informed public
- Free
Organizer
- LARA group
Cornilleau Pierre-Emmanuel
Viktor Kuncak
Contact
- Cornilleau Pierre-Emmanuel