Sciweavers

TPHOL
2007
IEEE

Proof Pearl: The Termination Analysis of Terminator

13 years 8 months ago
Proof Pearl: The Termination Analysis of Terminator
Terminator is a static analysis tool developed by Microsoft Research for proving termination of Windows device drivers written in C. This proof pearl describes a formalization in higher order logic of the program analysis employed by Terminator, and verifies that if the analysis succeeds then program termination logically follows.
Joe Hurd
Added 04 Jun 2010
Updated 04 Jun 2010
Type Conference
Year 2007
Where TPHOL
Authors Joe Hurd
Comments (0)