Name
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 a solution or targeted to specific theories, we propose a generic and radically new approach based on a reduction to the quantifier-free case. Our technique thus allows to reuse all the efficient machinery developed for that context. Experiments show a substantial improvement over state-of-the-art methods. |
Year | DOI | Venue |
|---|---|---|
2018 | 10.1007/978-3-319-96142-2_19 | COMPUTER AIDED VERIFICATION, CAV 2018, PT II |
DocType | Volume | ISSN |
Conference | 10982 | 0302-9743 |
Citations | PageRank | References |
1 | 0.35 | 25 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Benjamin Farinier | 1 | 1 | 0.35 |
| Sébastien Bardin | 2 | 297 | 19.35 |
| Richard Bonichon | 3 | 6 | 2.17 |
| Marie-Laure Potet | 4 | 190 | 21.34 |