HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/inria-00091655
Contributor : Stephan Merz Connect in order to contact the contributor
Submitted on : Friday, September 8, 2006 - 4:52:39 PM
Last modification on : Friday, September 8, 2006 - 4:53:14 PM
Long-term archiving on: : Thursday, September 20, 2012 - 10:20:37 AM

File

Identifiers

  • HAL Id : inria-00091655, version 1

Collections

Citation

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

Share

Metrics

Record views

32

Files downloads

13