Automatic Termination Proofs for Software - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2006

Automatic Termination Proofs for Software

Résumé

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.
Fichier principal
Vignette du fichier
cook.pdf (29.67 Ko) Télécharger le fichier

Dates et versions

inria-00091655 , version 1 (08-09-2006)

Identifiants

  • HAL Id : inria-00091655 , version 1

Citer

Byron Cook. Automatic Termination Proofs for Software. Automatic Verification of Critical Systems, Sep 2006, Nancy/France, pp.2. ⟨inria-00091655⟩

Collections

AVOCS06
41 Consultations
16 Téléchargements

Partager

Gmail Facebook X LinkedIn More