Détails sur le séminaire

salle 206
19 mars 2018 - 14h00
Model Generation for Quantified Formulas: A Taint-Based Approach
par Benjamin Farinier de CEA_LIST-SaClay



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.

Travaux conjoints : Benjamin Farinier, Sébastien Bardin, Richard Bonichon, Marie-Laure Potet




Contact | Plan du site | Site réalisé avec SPIP 3.0.26 + AHUNTSIC [CC License]

info visites 1077475