18 citations · 21 across the 4 of their papers we have counts for
Showing cs.LOShow all
2 papers · 1 filter
cs.LO2018
Model Generation for Quantified Formulas: A Taint-Based Approach
Benjamin Farinier, Sébastien Bardin, Richard Bonichon +1
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 m…
cs.LO2015
A syntactic soundness proof for free-variable tableaux with on-the-fly Skolemization
Richard Bonichon, Olivier Hermant
We prove the syntactic soundness of classical tableaux with free variables and on-the-fly Skolemization. Soundness proofs are usually built from semantic arguments, and this is to…