Help Privacy Policy Disclaimer
  Advanced SearchBrowse




Conference Paper

Termination Proofs for Systems Code


Podelski,  Andreas
Programming Logics, MPI for Informatics, Max Planck Society;


Rybalchenko,  Andrey
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)
There are no public fulltexts stored in PuRe
Supplementary Material (public)
There is no public supplementary material available

Cook, B., Podelski, A., & Rybalchenko, A. (2006). Termination Proofs for Systems Code. In PLDI 2006 : Proceedings of the ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation (pp. 415-426). New York, USA: ACM.

Cite as: https://hdl.handle.net/11858/00-001M-0000-000F-2416-9
Program termination is central to the process of ensuring that systems code can always react. We describe a new program termination prover that performs a path-sensitive and context-sensitive program analysis and provides capacity for large program fragments (i.e. more than 20,000 lines of code) together with support for programming language features such as arbitrarily nested loops, pointers, function-pointers, side-effects, etc.We also present experimental results on device driver dispatch routines from theWindows operating system. The most distinguishing aspect of our tool is how it shifts the balance between the two tasks of constructing and respectively checking the termination argument. Checking becomes the hard step. In this paper we show how we solve the corresponding challenge of checking with binary reachability analysis.