Termination proofs for systems code

ABSTRACT

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.

REFERENCES

• 1: I. Balaban, A. Pnueli, and L. D. Zuck. Shape analysis by predicate abstraction. In VMCAI'2005: Verification, Model Checking, and Abstract Interpretation, volume 3385 of LNCS. Springer, 2005.
• 2: T. Ball, E. Bounimova, B. Cook, V. Levin, J. Lichtenberg, C. McGarvey, B. Ondrusek, S. K. Rajamani, and A. Ustuner. Thorough static analysis of device drivers. In EuroSys'06: European Systems Conference, 2006.
• 3: A. Biere, C. Artho, and V. Schuppan. Liveness checking as safety checking. In FMICS'02: Formal Methods for Industrial Critical Systems, volume 66(2) of ENTCS, 2002.
• 4: Bruno Blanchet , Patrick Cousot , Radhia Cousot , Jérome Feret , Laurent Mauborgne , Antoine Miné , David Monniaux , Xavier Rival, A static analyzer for large safety-critical software, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 5: François Bourdoncle, Abstract debugging of higher-order imperative languages, Proceedings of the ACM SIGPLAN 1993 conference on Programming language design and implementation, p.46-55, June 21-25, 1993, Albuquerque, New Mexico, United States
• 6: A. Bradley, Z. Manna, and H. Sipma. Linear ranking with reachability. In CAV'05: Conference on Computer Aided Verification, volume 3576 of LNCS. Springer, 2005.
• 7: A. Bradley, Z. Manna, and H. Sipma. Termination of polynomial programs. In VMCAI'2005: Verification, Model Checking, and Abstract Interpretation, volume 3385 of LNCS. Springer, 2005.
• 8: E. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In TACAS'04: Tools and Algorithms for the Construction and Analysis of Systems, volume 2988 of LNCS, pages 168--176. Springer, 2004.
• 9: M. Codish and C. Taboch. A semantic basis for the termination analysis of logic programs. The Journal of Logic Programming, 41(1):103--123, 1999.
• 10: Michael Colón , Henny Sipma, Practical Methods for Proving Program Termination, Proceedings of the 14th International Conference on Computer Aided Verification, p.442-454, July 27-31, 2002
• 11: E. Contejean, C. Marché, B. Monate, and X. Urbain. Proving Termination of Rewriting with CiME. In Extended Abstracts of the 6th International Workshop on Termination, WST'03, pages 71--73, June 2003.
• 12: B. Cook, D. Kroening, and N. Sharygina. Cogent: Accurate theorem proving for program verification. In CAV'05: Conference on Computer Aided Verification, 2005.
• 13: B. Cook, A. Podelski, and A. Rybalchenko. Abstraction refinement for termination. In SAS'2005: Static Analysis Symposium, volume 3672 of LNCS, pages 87--101. Springer, 2005.
• 14: P. Cousot. Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In VMCAI'2005: Verification, Model Checking, and Abstract Interpretation, volume 3385 of LNCS. Springer, 2005.
• 15: R. W. Floyd. Assigning meanings to programs. In J. T. Schwartz, editor, Mathematical Aspects of Computer Science, volume 19 of Proceedings of Symposia in Applied Mathematics, pages 19--32. American Mathematical Society, 1967.
• 16: J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke. Automated termination proofs with AProVE. In RTA'2004: Rewriting Techniques and Applications, volume 3091 of LNCS, pages 210--220. Springer, 2004.
• 17: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Kenneth L. McMillan, Abstractions from proofs, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.232-244, January 14-16, 2004, Venice, Italy
• 18: Chin Soon Lee , Neil D. Jones , Amir M. Ben-Amram, The size-change principle for program termination, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.81-92, January 2001, London, United Kingdom
• 19: Naomi Lindenstrauss , Yehoshua Sagiv , Alexander Serebrenik, TermiLog: A System for Checking Termination of Queries to Logic Programs, Proceedings of the 9th International Conference on Computer Aided Verification, p.444-447, June 22-25, 1997
• 20: Zohar Manna , Amir Pnueli, Temporal verification of reactive systems: safety, Springer-Verlag New York, Inc., New York, NY, 1995
• 21: Microsoft Corporation. Windows Static Driver Verifier. Available at www.microsoft.com/whdc/devtools/tools/SDV.mspx, July 2004.
• 22: A. Podelski and A. Rybalchenko. A complete method for the synthesis of linear ranking functions. In VMCAI'2004: Verification, Model Checking, and Abstract Interpretation, volume 2937 of LNCS, pages 239--251. Springer, 2004.
• 23: Andreas Podelski , Andrey Rybalchenko, Transition Invariants, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04), p.32-41, July 13-17, 2004 [doi>10.1109/LICS.2004.50]
• 24: A. Turing. On computable numbers, with an application to the Entscheidungsproblem. London Mathematical Society, 42(2):230--265, 1936.
• 25: E. Yahav, T. Reps, M. Sagiv, and R.Wilhelm. Verifying temporal heap properties specified via evolution logic. In ESOP'2003: European Symp. on Programming, volume 2618 of LNCS, pages 204--222. Springer, 2003.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  D. Software
  D.4 OPERATING SYSTEMS
      D.4.5 Reliability

General Terms:
Reliability, Verification

Keywords:
formal verification, model checking, program termination, program verification