Skip to main content
Conference Proceedings

Proof pearl: The termination analysis of TERMINATOR

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (2007) 4732 LNCS 151-156
DOI: 10.1007/978-3-540-74591-4_12
0Citations
Citations of this article
2Readers
Mendeley users who have this article in their library.
Get full text

Abstract

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. © Springer-Verlag Berlin Heidelberg 2007.

Cite

CITATION STYLE

APA

Hurd, J. (2007). Proof pearl: The termination analysis of TERMINATOR. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4732 LNCS, pp. 151–156). Springer Verlag. https://doi.org/10.1007/978-3-540-74591-4_12

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free