On Quantitative Software Verification

Abstract : Software verification has made great progress in recent years, resulting in several tools capable of working directly from source code, for example, SLAM and Astree. Typical properties that can be verified are expressed as Boolean assertions or temporal logic properties, and include whether the program eventually terminates, or the executions never violate a safety property. The underlying techniques crucially rely on the ability to extract from programs, using compiler tools and predicate abstraction, finite-state abstract models, which are then iteratively refined to either demonstrate the violation of a safety property (e.g. a buffer overflow) or guarantee the absence of such faults. An established method to achieve this automatically executes an abstraction-refinement loop guided by counterexample traces [1].
Type de document :
Communication dans un congrès
Corina S. Păsăreanu. SPIN 2009 : Model Checking Software, 16th International SPIN Workshop, Jun 2009, Grenoble, France. Springer, 5578, pp.2-3, 2009, Lecture Notes in Computer Science. 〈10.1007/978-3-642-02652-2〉
Liste complète des métadonnées

Littérature citée [4 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00457746
Contributeur : Brigitte Briot <>
Soumis le : jeudi 18 février 2010 - 13:26:36
Dernière modification le : vendredi 26 février 2010 - 14:10:22
Document(s) archivé(s) le : vendredi 18 juin 2010 - 21:18:35

Fichier

spin09.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Marta Kwiatkowska. On Quantitative Software Verification. Corina S. Păsăreanu. SPIN 2009 : Model Checking Software, 16th International SPIN Workshop, Jun 2009, Grenoble, France. Springer, 5578, pp.2-3, 2009, Lecture Notes in Computer Science. 〈10.1007/978-3-642-02652-2〉. 〈inria-00457746〉

Partager

Métriques

Consultations de la notice

72

Téléchargements de fichiers

93