@inproceedings{1feeae780a3f42d8a60f04e33d3114eb,
title = "Static versus dynamic verification in Why3, Frama-C and SPARK 2014",
abstract = "Why3 is an environment for static verification, generic in the sense that it is used as an intermediate tool by different front-ends for the verification of Java, C or Ada programs. Yet, the choices made when designing the specification languages provided by those front-ends differ significantly, in particular with respect to the executability of specifications. We review these differences and the issues that result from these choices. We emphasize the specific feature of ghost code which turns out to be extremely useful for both static and dynamic verification. We also present techniques, combining static and dynamic features, that help users understand why static verification fails.",
author = "Nikolai Kosmatov and Claude March{\'e} and Yannick Moy and Julien Signoles",
note = "Publisher Copyright: {\textcopyright} Springer International Publishing AG 2016.; 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2016 ; Conference date: 10-10-2016 Through 14-10-2016",
year = "2016",
month = jan,
day = "1",
doi = "10.1007/978-3-319-47166-2\_32",
language = "English",
isbn = "9783319471655",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "461--478",
editor = "Tiziana Margaria and Bernhard Steffen",
booktitle = "Leveraging Applications of Formal Methods, Verification and Validation",
}