Model Generation for Quantified Formulas: A Taint-Based Approach - Archive ouverte HAL Access content directly
Preprints, Working Papers, ... Year :

Model Generation for Quantified Formulas: A Taint-Based Approach

(1, 2) , (1) , (1) , (2)
1
2
Benjamin Farinier
  • Function : Author
  • PersonId : 962753
Sébastien Bardin
  • Function : Author
  • PersonId : 755498
  • IdRef : 161083781
Richard Bonichon
  • Function : Author
  • PersonId : 1005710
Marie-Laure Potet
  • Function : Author

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.
Fichier principal
Vignette du fichier
cav2018.pdf (368.86 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

cea-01709306 , version 1 (14-02-2018)

Identifiers

Cite

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

Altmetric

Share

Gmail Facebook Twitter LinkedIn More