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.

• Type: Conference
• Year: 2007
• Where: TPHOL
• Authors: Joe Hurd
• Keywords: Artificial Intelligence, Program Termination, Static Analysis Tool, TPHOL 2007, Windows Device Drivers