FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Model Generation for Quantified Formulas: A Taint-Based Approach

Authors: Benjamin Farinier, Sebastien Bardin, Richard Bonichon and Marie-Laure Potet

Paper Information

Title:Model Generation for Quantified Formulas: A Taint-Based Approach
Authors:Benjamin Farinier, Sebastien Bardin, Richard Bonichon and Marie-Laure Potet
Proceedings:CAV All Papers
Editors: Georg Weissenbacher, Hana Chockler and Igor Konnov
Keywords:automated reasoning, first-order logic, model generation
Abstract:

ABSTRACT. We focus in this paper on generating models of quantified first-order formulas over built-in theories, which is paramount in software verification and bug finding. While standard methods are either geared toward proving the absence of solution or targeted to specific theories, we propose a generic approach based on a reduction to the quantifier-free case. Our technique allows thus to reuse all the efficient machinery developed for that context. Experiments show a substantial improvement over state-of-the-art methods.

Pages:19
Talk:Jul 17 12:00 (Session 119A: SAT, SMT and Decision Procedures)
Paper: