Byron Cook
Andreas Podelski
Moshe Y. Vardi
Skip Abstract Section
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.
- Albin et al. Property specification language reference manual. Tech. Rep. Version 1.1, Accellera, 2004.Google Scholar
- Alpern, B., and Schneider, F. Defining liveness. Information processing letters 21 (1985), 181--185.Google Scholar
- Alpern, B., and Schneider, F. Recognizing safety and liveness. Distributed computing 2 (1987), 117--126.Google Scholar
- Armoni, R., Fix, L., Flaisher, A., Gerth, R., Ginsburg, B., Kanza, T., Landver, A., Mador-Haim, S., Singerman, E., Tiemeyer, A., Vardi, M., and Zbar, Y. The ForSpec temporal logic: A new temporal property-specification logic. In TACAS'02: Tools and Algorithms for the Construction and Analysis of Systems (2002), vol. 2280 of LNCS, Springer-Verlag, pp. 296--311. Google ScholarDigital Library
- Ball, T., Bounimova, E., Cook, B., Levin, V., Lichtenberg, J., McGarvey, C., Ondrusek, B., Rajamani, S. K., and Ustuner, A. Thorough static analysis of device drivers. In EuroSys'06: European Systems Conference (2006). Google ScholarDigital Library
- Ball, T., and Rajamani, S. K. SLIC: A specification language for interface checking (of C). Tech. Rep. MSR-TR-2001-21, Microsoft Research, 2001.Google Scholar
- Berdine, J., Chawdhary, A., Cook, B., Distefano, D., and O'Hearn, P. Variance analyses from invariance analyses. In POPL'07: Principles of Programming Languages (2007), ACM Press. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Colón, M. A., and Uribe, T. E. Generating finite-state abstractions of reactive systems using decision procedures. In CAV 98: Computer-Aided Verification (1998), vol. 1427 of LNCS, Springer-Verlag, pp. 293--304. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Cook, B., Podelski, A., and Rybalchenko, A. Termination proofs for systems code. In PLDI'06: Programming Language Design and Implementation (2006), ACM Press, pp. 415--426. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Corbett, J., Dwyer, M., Hatcliff, J., Pasareanu, C., Robby, Laubach, S., and Zheng, H. Bandera: Extracting finite-state models from Java source code. In ICSE'00: Int. Conf. on Software Engineering (2000), IEEE Press, pp. 439--448. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Dwyer, M. B., Avrunin, G. S., and Corbett, J. C. Patterns in property specifications for finite-state verification. In ICSE'99: Int. Conf. on Software Engineering (1999), IEEE Press, pp. 411--420. Google ScholarDigital Library
- 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.Google Scholar
- Graf, S., and Saïdi, H. Construction of abstract state graphs with PVS. In CAV 97: Computer-Aided Verification (1997), vol. 1254 of LNCS, Springer-Verlag, pp. 72--83. Google ScholarDigital Library
- Henzinger, T., Jhala, R., Majumdar, R., and Sutre, G. Lazy abstraction. In POPL'02: Principles of Programming Languages (2002), ACM Press, pp. 58--70. Google ScholarDigital Library
- Holzmann, G. J. The model checker SPIN. IEEE Transactions on Software Engineering 23, 5 (1997), 279--295. Google ScholarDigital Library
- Kesten, Y., Pnueli, A., and Raviv, L. Algorithmic verification of linear temporal logic specifications. In ICALP'98: Int. Colloq. on Automata, Languages and Programming (1998), vol. 1443 of LNCS, Springer-Verlag, pp. 1--16. Google ScholarDigital Library
- Kurshan, R. Computer Aided Verification of Coordinating Processes. Princeton Univ. Press, 1994. Google ScholarDigital Library
- Manna, Z., and Pnueli, A. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, Berlin, 1992. Google ScholarDigital Library
- Microsoft Corporation. Windows Static Driver Verifier. Available at www.microsoft.com/whdc/devtools/tools/SDV.mspx, July 2006.Google Scholar
- Pnueli, A. The temporal logic of programs. In Proc. 18th IEEE Symp. on Foundation of Computer Science (1977), pp. 46--57.Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google Scholar
- Podelski, A., and Rybalchenko, A. Transition invariants. In LICS'04: Logic in Computer Science (2004), LNCS, IEEE Press, pp. 32--41. Google ScholarDigital Library
- Vardi, M. Verification of concurrent programs---the automata-theoretic framework. Annals of Pure and Applied Logic 51/ (1991), 79--98.Google ScholarCross Ref
- Vardi, M., and Wolper, P. Reasoning about infinite computations. Information and Computation 115, 1 (1994), 1--37. Google ScholarDigital Library
- Visser, W., Havelund, K., Brat, G., Park, S., and Lerda, F. Model checking programs. Automated Software Engineering Journal 10, 2 (2003). Google ScholarDigital Library
Index Terms
- Proving that programs eventually do something good
Recommendations
Proving that programs eventually do something good
POPL '07: Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesIn 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). ...
Transition predicate abstraction and fair termination
POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languagesPredicate abstraction is the basis of many program verification tools. Until now, the only known way to overcome the inherent limitation of predicate abstraction to safety properties was to manually annotate the finite-state abstraction of a program. We ...
Transition predicate abstraction and fair termination
Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languagesPredicate abstraction is the basis of many program verification tools. Until now, the only known way to overcome the inherent limitation of predicate abstraction to safety properties was to manually annotate the finite-state abstraction of a program. We ...
Comments