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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Ball, T., Bounimova, E., Cook, B., Levin, V., Lichtenberg, J., McGarvey, C., Ondrusek, B., Rajamani, S.K., Ustuner, A.: Thorough static analysis of device drivers. In: Proceedings of the EuroSys 2006 Conference, April 2006, pp. 73–85 (2006)
Cook, B., Podelski, A., Rybalchenko, A.: Terminator: Beyond safety. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 415–418. Springer, Heidelberg (2006)
Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL (A theorem-proving environment for higher order logic). Cambridge University Press, Cambridge (1993)
Landman, B.M., Robertson, A.: Ramsey Theory on the Integers, February 2004. American Mathematical Society, Providence, RI (2004)
Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 239–251. Springer, Heidelberg (2004)
Podelski, A., Rybalchenko, A.: Transition invariants. In: 19th IEEE Symposium on Logic in Computer Science (LICS 2004), July 2004, pp. 32–41. IEEE Computer Society Press, Los Alamitos (2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hurd, J. (2007). Proof Pearl: The Termination Analysis of Terminator . In: Schneider, K., Brandt, J. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2007. Lecture Notes in Computer Science, vol 4732. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74591-4_12
Download citation
DOI: https://doi.org/10.1007/978-3-540-74591-4_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74590-7
Online ISBN: 978-3-540-74591-4
eBook Packages: Computer ScienceComputer Science (R0)