Proving that programs eventually do something good

ABSTRACT

In recent years we have seen great progress made in the area of automatic source-level static analysis tools. However, most of today's program verification tools are limited to properties that guarantee the absence of bad events (safety properties). Until now no formal software analysis tool has provided fully automatic support for proving properties that ensure that good events eventually happen (liveness properties). In this paper we present such a tool, which handles liveness properties of large systems written in C. Liveness properties are described in an extension of the specification language used in the SDV system. We have used the tool to automatically prove critical liveness properties of Windows device drivers and found several previously unknown liveness bugs.

REFERENCES

• 1: Albin et al. Property specification language reference manual. Tech. Rep. Version 1.1, Accellera, 2004.
• 2: Alpern, B., and Schneider, F. Defining liveness. Information processing letters 21 (1985), 181--185.
• 3: Alpern, B., and Schneider, F. Recognizing safety and liveness. Distributed computing 2 (1987), 117--126.
• 4: Roy Armoni , Limor Fix , Alon Flaisher , Rob Gerth , Boris Ginsburg , Tomer Kanza , Avner Landver , Sela Mador-Haim , Eli Singerman , Andreas Tiemeyer , Moshe Y. Vardi , Yael Zbar, The ForSpec Temporal Logic: A New Temporal Property-Specification Language, Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.296-211, April 08-12, 2002
• 5: Thomas Ball , Ella Bounimova , Byron Cook , Vladimir Levin , Jakob Lichtenberg , Con McGarvey , Bohus Ondrusek , Sriram K. Rajamani , Abdullah Ustuner, Thorough static analysis of device drivers, Proceedings of the 2006 EuroSys conference, April 18-21, 2006, Leuven, Belgium
• 6: Ball, T., and Rajamani, S. K. SLIC: A specification language for interface checking (of C). Tech. Rep. MSR-TR-2001-21, Microsoft Research, 2001.
• 7: Josh Berdine , Aziem Chawdhary , Byron Cook , Dino Distefano , Peter O'Hearn, Variance analyses from invariance analyses, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France
• 8: Berdine, J., Cook, B., Distefano, D., and O'Hearn, P. Automatic termination proofs for programs with shape-shifting heaps. In CAV'06: Computer-Aided Verification (2006), vol. 4144 of LNCS, Springer-Verlag, pp. 386--400.
• 9: Biere, A., Artho, C., and Schuppan, V. Liveness checking as safety checking. In FMICS'02: Formal Methods for Industrial Critical Systems (2002), vol. 66(2) of ENTCS.
• 10: Bradley, A., Manna, Z., and Sipma, H. Linear ranking with reachability. In CAV'05: Computer-Aided Verification (2005), vol. 3576 of LNCS, Springer-Verlag, pp. 491--504.
• 11: Bradley, A., Manna, Z., and Sipma, H. Termination of polynomial programs. In VMCAI'05: Verification, Model Checking, and Abstract Interpretation (2005), vol. 3385 of LNCS, Springer-Verlag, pp. 113--129.
• 12: Michael Colón , Tomás E. Uribe, Generating Finite-State Abstractions of Reactive Systems Using Decision Procedures, Proceedings of the 10th International Conference on Computer Aided Verification, p.293-304, June 28-July 02, 1998
• 13: Cook, B., Podelski, A., and Rybalchenko, A. Abstraction refinement for termination. In SAS'05: Static Analysis Symposium (2005), vol. 3672 of LNCS, Springer-Verlag, pp. 87--101.
• 14: Byron Cook , Andreas Podelski , Andrey Rybalchenko, Termination proofs for systems code, Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, June 11-14, 2006, Ottawa, Ontario, Canada
• 15: Cook, B., Podelski, A., and Rybalchenko, A. Terminator: Beyond safety. In CAV'06: Computer-Aided Verification (2006), vol. 4144 of LNCS, Springer-Verlag, pp. 415--418.
• 16: James C. Corbett , Matthew B. Dwyer , John Hatcliff , Shawn Laubach , Corina S. Păsăreanu , Robby , Hongjun Zheng, Bandera: extracting finite-state models from Java source code, Proceedings of the 22nd international conference on Software engineering, p.439-448, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337234]
• 17: Cousot, P. Proving program invariance and termination by parametric abstraction, Lagrangian relaxation and semidefinite programming. In VMCAI'05: Verification, Model Checking, and Abstract Interpretation (2005), vol. 3385 of LNCS, Springer-Verlag, pp. 1--24.
• 18: Matthew B. Dwyer , George S. Avrunin , James C. Corbett, Patterns in property specifications for finite-state verification, Proceedings of the 21st international conference on Software engineering, p.411-420, May 16-22, 1999, Los Angeles, California, United States [doi>10.1145/302405.302672]
• 19: Floyd, R. W. Assigning meanings to programs. In Mathematical Aspects of Computer Science (1967), J. T. Schwartz, Ed., vol. 19 of Proceedings of Symposia in Applied Mathematics, American Mathematical Society, pp. 19--32.
• 20: Susanne Graf , Hassen Saïdi, Construction of Abstract State Graphs with PVS, Proceedings of the 9th International Conference on Computer Aided Verification, p.72-83, June 22-25, 1997
• 21: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Grégoire Sutre, Lazy abstraction, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.58-70, January 16-18, 2002, Portland, Oregon
• 22: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 23: Yonit Kesten , Amir Pnueli , Li-on Raviv, Algorithmic Verification of Linear Temporal Logic Specifications, Proceedings of the 25th International Colloquium on Automata, Languages and Programming, p.1-16, July 13-17, 1998
• 24: Robert P. Kurshan, Computer-aided verification of coordinating processes: the automata-theoretic approach, Princeton University Press, Princeton, NJ, 1994
• 25: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 26: Microsoft Corporation. Windows Static Driver Verifier. Available at www.microsoft.com/whdc/devtools/tools/SDV.mspx, July 2006.
• 27: Pnueli, A. The temporal logic of programs. In Proc. 18th IEEE Symp. on Foundation of Computer Science (1977), pp. 46--57.
• 28: Pnueli, A., Podelski, A., and Rybalchenko, A. Separating fairness and well-foundedness for the analysis of fair discrete systems. In TACAS'05: Tools and Algorithms for the Construction and Analysis of Systems (2005), vol. 3440 of LNCS, Springer-Verlag, pp. 124--139.
• 29: Podelski, A., and Rybalchenko, A. A complete method for the synthesis of linear ranking functions. In VMCAI'04: Verification, Model Checking, and Abstract Interpretation (2004), vol. 2937 of LNCS, Springer-Verlag, pp. 239--251.
• 30: 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]
• 31: Vardi, M. Verification of concurrent programs---the automata-theoretic framework. Annals of Pure and Applied Logic 51/ (1991), 79--98.
• 32: Moshe Y. Vardi , Pierre Wolper, Reasoning about infinite computations, Information and Computation, v.115 n.1, p.1-37, Nov. 15, 1994 [doi>10.1006/inco.1994.1092]
• 33: Willem Visser , Klaus Havelund , Guillaume Brat , Seungjoon Park , Flavio Lerda, Model Checking Programs, Automated Software Engineering, v.10 n.2, p.203-232, April 2003 [doi>10.1023/A:1022920129859]

INDEX TERMS

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

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Languages, Reliability, Verification

Keywords:
formal verification, liveness, software model checking, termination