Model Generation for Quantified Formulas: A Taint-Based Approach

Benjamin Farinier (1, 2) , Sébastien Bardin (1) , Richard Bonichon (1) , Marie-Laure Potet (2)

1 LSL - Laboratoire Sûreté des Logiciels
2 VERIMAG - IMAG - VERIMAG

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.

Keywords: automated reasoning; first-order logic; model generation

Domains: Logic in Computer Science [cs.LO]

Benjamin Farinier, Sébastien Bardin, Richard Bonichon, Marie-Laure Potet. Model Generation for Quantified Formulas: A Taint-Based Approach. 2018. ⟨cea-01709306⟩