Skip to Main content Skip to Navigation
Conference papers

Static versus Dynamic Verification in Why3, Frama-C and SPARK 2014

Nikolai Kosmatov 1 Claude Marché 2, 3 Yannick Moy 4 Julien Signoles 1
1 LSL - Laboratoire Sûreté des Logiciels
DILS - Département Ingénierie Logiciels et Systèmes : DRT/LIST/DILS
3 TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations
LRI - Laboratoire de Recherche en Informatique, Inria Saclay - Ile de France
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.
Document type :
Conference papers
Complete list of metadata

Cited literature [43 references]  Display  Hide  Download
Contributor : Claude Marché Connect in order to contact the contributor
Submitted on : Monday, July 11, 2016 - 1:14:55 PM
Last modification on : Thursday, July 8, 2021 - 3:52:29 AM


Files produced by the author(s)


  • HAL Id : hal-01344110, version 1


Nikolai Kosmatov, Claude Marché, Yannick Moy, Julien Signoles. Static versus Dynamic Verification in Why3, Frama-C and SPARK 2014. 7th International Symposium on Leveraging Applications, Oct 2016, Corfu, Greece. pp.461--478. ⟨hal-01344110⟩



Record views


Files downloads