Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

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
DILS - Département Ingénierie Logiciels et Systèmes : DRT/LIST/DILS
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.
Document type :
Preprints, Working Papers, ...
Complete list of metadata

Cited literature [30 references]  Display  Hide  Download

https://hal-cea.archives-ouvertes.fr/cea-01709306
Contributor : Benjamin Farinier <>
Submitted on : Wednesday, February 14, 2018 - 6:33:17 PM
Last modification on : Friday, November 20, 2020 - 1:08:01 PM
Long-term archiving on: : Monday, May 7, 2018 - 4:16:59 AM

Files

cav2018.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : cea-01709306, version 1
  • ARXIV : 1802.05616

Collections

Citation

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

Share

Metrics

Record views

335

Files downloads

338