Automatic Termination Proofs for Software

Abstract : In this talk I will describe recent advances in the area of automatic program termination analysis. In particular, I will describe the development of several automatic tools, called Terminator and Mutant, which implement new termination analysis algorithms. These tools have been used to prove that Windows device driver dispatch routines always return control back to their caller. The tools have also found a number of critical termination bugs in device drivers.
Type de document :
Communication dans un congrès
Stephan Merz and Tobias Nipkow. Automatic Verification of Critical Systems, Sep 2006, Nancy/France, pp.2, 2006, Automatic Verification of Critical Systems (AVoCS 2006)
Liste complète des métadonnées

https://hal.inria.fr/inria-00091655
Contributeur : Stephan Merz <>
Soumis le : vendredi 8 septembre 2006 - 16:52:39
Dernière modification le : vendredi 8 septembre 2006 - 16:53:14
Document(s) archivé(s) le : jeudi 20 septembre 2012 - 10:20:37

Fichier

Identifiants

  • HAL Id : inria-00091655, version 1

Collections

Citation

Byron Cook. Automatic Termination Proofs for Software. Stephan Merz and Tobias Nipkow. Automatic Verification of Critical Systems, Sep 2006, Nancy/France, pp.2, 2006, Automatic Verification of Critical Systems (AVoCS 2006). 〈inria-00091655〉

Partager

Métriques

Consultations de la notice

66

Téléchargements de fichiers

43