Correct Code Containing Containers

Claire Dross 1, 2 Jean-Christophe Filliâtre 1, 2 Yannick Moy 3
2 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : For critical software development, containers such as lists, vectors, sets or maps are an attractive alternative to ad-hoc data structures based on pointers. As standards like DO-178C put formal verification and testing on an equal footing, it is important to give users the ability to apply both to the verification of code using containers. In this paper, we present a definition of containers whose aim is to facilitate their use in certified software, using modern proof technology and novel specification languages. Correct usage of containers and user-provided correctness properties can be checked either by execution during testing or by formal proof with an automatic prover. We present a formal semantics for containers and an axiomatization of this semantics targeted at automatic provers. We have proved in Coq that the formal semantics is consistent and that the axiomatization thereof is correct.
Type de document :
Communication dans un congrès
TAP - 5th International Conference on Tests and Proofs, 2011, Zurich, Switzerland. 2011
Liste complète des métadonnées

Littérature citée [13 références]  Voir  Masquer  Télécharger
Contributeur : Claude Marché <>
Soumis le : jeudi 17 janvier 2013 - 17:44:53
Dernière modification le : jeudi 9 février 2017 - 15:43:34
Document(s) archivé(s) le : jeudi 18 avril 2013 - 04:02:10


Fichiers produits par l'(les) auteur(s)


  • HAL Id : hal-00777683, version 1



Claire Dross, Jean-Christophe Filliâtre, Yannick Moy. Correct Code Containing Containers. TAP - 5th International Conference on Tests and Proofs, 2011, Zurich, Switzerland. 2011. 〈hal-00777683〉



Consultations de
la notice


Téléchargements du document