More Web Proxy on the site http://driver.im/

Article

Proving that programs eventually do something good

Authors:

Alexey Gotsman,

Andreas Podelski,

Andrey Rybalchenko,

Moshe Y. VardiAuthors Info & Claims

POPL '07: Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 265 - 276

https://doi.org/10.1145/1190216.1190257

Published: 17 January 2007 Publication History

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]

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.

Digital Library

[5]

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).

Digital Library

[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]

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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[12]

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.

Digital Library

[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.

Digital Library

[14]

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.

Digital Library

[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.

Digital Library

[16]

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.

Digital Library

[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.

Digital Library

[18]

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.

Digital Library

[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]

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.

Digital Library

[21]

Henzinger, T., Jhala, R., Majumdar, R., and Sutre, G. Lazy abstraction. In POPL'02: Principles of Programming Languages (2002), ACM Press, pp. 58--70.

Digital Library

[22]

Holzmann, G. J. The model checker SPIN. IEEE Transactions on Software Engineering 23, 5 (1997), 279--295.

Digital Library

[23]

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.

Digital Library

[24]

Kurshan, R. Computer Aided Verification of Coordinating Processes. Princeton Univ. Press, 1994.

Digital Library

[25]

Manna, Z., and Pnueli, A. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, Berlin, 1992.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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]

Podelski, A., and Rybalchenko, A. Transition invariants. In LICS'04: Logic in Computer Science (2004), LNCS, IEEE Press, pp. 32--41.

Digital Library

[31]

Vardi, M. Verification of concurrent programs---the automata-theoretic framework. Annals of Pure and Applied Logic 51/ (1991), 79--98.

[32]

Vardi, M., and Wolper, P. Reasoning about infinite computations. Information and Computation 115, 1 (1994), 1--37.

Digital Library

[33]

Visser, W., Havelund, K., Brat, G., Park, S., and Lerda, F. Model checking programs. Automated Software Engineering Journal 10, 2 (2003).

Digital Library

Cited By

Yao JTao RGu RNieh J(2024)Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking FunctionsProceedings of the ACM on Programming Languages10.1145/36328778:POPL(1028-1059)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632877
Abate AGiacobbe MRoy DSchnitzer Y(2024)Model Checking and Strategy Synthesis with Abstractions and CertificatesPrinciples of Verification: Cycling the Probabilistic Landscape10.1007/978-3-031-75775-4_16(360-391)Online publication date: 13-Nov-2024
https://doi.org/10.1007/978-3-031-75775-4_16
Jochems JJones ERamsay S(2023)Higher-Order MSL Horn ConstraintsProceedings of the ACM on Programming Languages10.1145/35712627:POPL(2017-2047)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571262
Show More Cited By

Index Terms

Proving that programs eventually do something good

Recommendations

Proving that programs eventually do something good
Proceedings of the 2007 POPL Conference

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). ...
Transition predicate abstraction and fair termination
POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Predicate 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 languages

Predicate 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

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '07: Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2007

400 pages

ISBN:1595935754

DOI:10.1145/1190216

General Chair:
Martin Hofmann
Ludwig-Maximilians U, Munich, Germany
,
Program Chair:
Matthias Felleisen
Northeastern University, Boston MA

ACM SIGPLAN Notices Volume 42, Issue 1
Proceedings of the 2007 POPL Conference
January 2007
379 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1190215
Issue’s Table of Contents

Copyright © 2007 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 17 January 2007

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

POPL07

Sponsor:

POPL07: The 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 17 - 19, 2007

Nice, France

Acceptance Rates

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

100
Total Citations
View Citations
912
Total Downloads

Downloads (Last 12 months)33
Downloads (Last 6 weeks)2

Reflects downloads up to 30 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Yao JTao RGu RNieh J(2024)Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking FunctionsProceedings of the ACM on Programming Languages10.1145/36328778:POPL(1028-1059)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632877
Abate AGiacobbe MRoy DSchnitzer Y(2024)Model Checking and Strategy Synthesis with Abstractions and CertificatesPrinciples of Verification: Cycling the Probabilistic Landscape10.1007/978-3-031-75775-4_16(360-391)Online publication date: 13-Nov-2024
https://doi.org/10.1007/978-3-031-75775-4_16
Jochems JJones ERamsay S(2023)Higher-Order MSL Horn ConstraintsProceedings of the ACM on Programming Languages10.1145/35712627:POPL(2017-2047)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571262
Kobayashi NTanahashi KSato RTsukada T(2023)HFL(Z) Validity Checking for Automated Program VerificationProceedings of the ACM on Programming Languages10.1145/35711997:POPL(154-184)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571199
Pani TWeissenbacher GZuleger F(2023)Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verificationFormal Methods in System Design10.1007/s10703-023-00439-664:1-3(108-145)Online publication date: 6-Oct-2023
https://doi.org/10.1007/s10703-023-00439-6
Ciccone LPadovani L(2022)Fair termination of binary sessionsProceedings of the ACM on Programming Languages10.1145/34986666:POPL(1-30)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498666
Kobayashi N(2021)An Overview of the HFL Model Checking ProjectElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.344.1344(1-12)Online publication date: 13-Sep-2021
https://doi.org/10.4204/EPTCS.344.1
Zhu SKincaid ZFreund SYahav E(2021)Termination analysis without the tearsProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3453483.3454110(1296-1311)Online publication date: 19-Jun-2021
https://dl.acm.org/doi/10.1145/3453483.3454110
Stephens JFerles KMariano BLahiri SDillig I(2021)SmartPulse: Automated Checking of Temporal Properties in Smart Contracts2021 IEEE Symposium on Security and Privacy (SP)10.1109/SP40001.2021.00085(555-571)Online publication date: May-2021
https://doi.org/10.1109/SP40001.2021.00085
Wang MTian CZhang NDuan Z(2019)Verifying Full Regular Temporal Properties of Programs via Dynamic Program ExecutionIEEE Transactions on Reliability10.1109/TR.2018.287633368:3(1101-1116)Online publication date: Sep-2019
https://doi.org/10.1109/TR.2018.2876333
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents