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 - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
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
Liste complète des métadonnées

Cited literature [43 references]  Display  Hide  Download

https://hal.inria.fr/hal-01344110
Contributor : Claude Marché <>
Submitted on : Monday, July 11, 2016 - 1:14:55 PM
Last modification on : Thursday, February 7, 2019 - 2:38:01 PM

File

paper063.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01344110, version 1

Citation

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⟩

Share

Metrics

Record views

1188

Files downloads

717