article

The pointer assertion logic engine

Authors:

Anders Møller,

Michael I. SchwartzbachAuthors Info & Claims

ACM SIGPLAN Notices, Volume 36, Issue 5

Pages 221 - 231

https://doi.org/10.1145/381694.378851

Published: 01 May 2001 Publication History

Abstract

We present a new framework for verifying partial specifications of programs in order to catch type and memory errors and check data structure invariants. Our technique can verify a large class of data structures, namely all those that can be expressed as graph types. Earlier versions were restricted to simple special cases such as lists or trees. Even so, our current implementation is as fast as the previous specialized tools.

Programs are annotated with partial specifications expressed in Pointer Assertion Logic, a new notation for expressing properties of the program store. We work in the logical tradition by encoding the programs and partial specifications as formulas in monadic second-order logic. Validity of these formulas is checked by the MONA tool, which also can provide explicit counterexamples to invalid formulas.

To make verification decidable, the technique requires explicit loop and function call invariants. In return, the technique is highly modular: every statement of a given program is analyzed only once.

The main target applications are safety-critical data-type algorithms, where the cost of annotating a program with invariants is justified by the value of being able to automatically verify complex properties of the program.

References

[1]

Krzyszt of R. Apt. Ten years of Hoare 's logic: A survey part I. ACM Transactions on Programming Languages 3(4):431-483, 1981.]]

Digital Library

[2]

Thomas Ball and Sriram K. Rajamani. Bebop: A symbolic model checker for boolean programs.In Proceedings of the SPIN Software Model Checking Workshop volume 1885 of LNCS 2000.]]

Digital Library

[3]

Michael Benedikt, Thomas Reps, and Mooly Sagiv. A decidable logic for describing lined data structures. In European Symposium On Programming, ESOP'99 volume 1576 of LNCS 1999.]]

Digital Library

[4]

Morten Biehl, Nils Klarlund, and Theis Rauhe. Algorithms for guided tree automata. In First International Workshop on Implementing Automata, WIA'96 volume 1260 of LNCS 1997.]]

Digital Library

[5]

Paul E. Blac and Phillip J. Windley. Inference rules for programming languages with side effects in expressions. In International Conference on Theorem Proving in Higher Order Logics 1996.]]

Digital Library

[6]

Randal E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers C-35(8):677-691, Aug 1986.]]

Digital Library

[7]

William R. Bush, Jonathan D. Pincus, and David J. Siela. A static analyzer for finding dynamic programming errors. Software: Practice and Experience 30(7), 2000.]]

Digital Library

[8]

Stephen A. Coo and Dere C. Oppen. An assertion language for data structures. In Principles of Programming Languages, POPL'75 pages 160-166, 1975.]]

Digital Library

[9]

C. Corbett, Matthew B. Dwyer, John Hatcli., and Robby. A language framework for expressing chec - able properties of dynamic software. In Proceedings of the SPIN Software Model Checking Workshop volume 1885 of LNCS 2000.]]

Digital Library

[10]

Thomas H. Cormen, Charles E. Leiserson, and Ronald L. Rivest. Introduction to Algorithms MIT Press, 1990.]]

Digital Library

[11]

Patric Cousot. Formal models and semantics. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science volume B, pages 841-993. MIT Press/Elsevier, 1990.]]

[12]

David L. Detlefs, K. Rustan M. Leino, Greg Nelson, and James B. Saxe. Extended static checking. Research Report 159, Compaq Systems Research Center, December, 1998.]]

[13]

Nurit Dor, Michael Rodeh, and Mooly Sagiv. Checking cleanness in lined lists. In Seventh International Static Analysis Symposium, SAS'00 2000.]]

Digital Library

[14]

Jacob Elgaard, Anders Moller, and Michael I. Schwartzbach. Compile-time debugging of C programs working on trees.In European Symposium on Programming Languages and Systems, ESOP'00 volume 1782 of LNCS 2000.]]

Digital Library

[15]

David Evans. Static detection of dynamic memory errors. In Programming Language Design and Implementation, PLDI'96 1996.]]

Digital Library

[16]

Robert W. Floyd. Assigning meanings to programs. Mathematical Aspects of Computer Science, American Math. Soc., 1967.]]

[17]

Pascal Fradet, Ronan Gaugne, and Daniel Le M~tayer. Static detection of pointer errors: An axiomatisation and a checking algorithm. In European Symposium on Programming, ESOP'96 volume 1058 of LNCS 1996.]]

Digital Library

[18]

Pascal Fradet and Daniel Le M~tayer. Shape types. In Principles of Programming Languages, POPL'97 ACM, 1997.]]

Digital Library

[19]

David Gries. The Science of Programming Springer- Verlag, 1981.]]

Digital Library

[20]

Klaus Havelund and Thomas Pressburger. Model checking Java programs using Java Path Finder. International Journal on Software Tools for Technology Transf er 2(4), April 2000.]]

[21]

Laurie Hendren, Joseph Hummel, and Alexandru Nicolau. Abstractions for recursive pointer data structures: Improving the analysis and transformation of imperative programs. In Program Language Design and Implementation, PLDI'92 1992.]]

Digital Library

[22]

C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM 12(10):576- 580, Oct 1969.]]

Digital Library

[23]

Daniel Jac son and Mandana Vaziri. Finding bugs with a constraint solver. In International Symposium on Software Testing and Analysis, ISSTA'00 ACM, 2000.]]

Digital Library

[24]

Jacob L. Jensen, Michael E. Jorgensen, Nils Klarlund, and Michael I. Schwartzbach. Automatic verification of pointer programs using monadic second-order logic. In Programming Language Design and Implementation, PLDI'97 1997.]]

Digital Library

[25]

Nils Klarlund. Mona & Fido: The logic-automaton connection in practice. In Computer Science Logic, CSL'97 volume 1414 of LNCS 1998.]]

Digital Library

[26]

Nils Klarlund and Anders Moller. MONA Version 1.4 User Manual BRICS Notes Series NS-01-1, Department of Computer Science, University of Aarhus, January 2001.]]

[27]

Nils Klarlund, Anders Moller, and Michael I. Schwartzbach. MONA implementation secrets. In Fifth International Conference on Implementation and Application of Automata, CIAA'00 LNCS, 2000.]]

Digital Library

[28]

Nils Klarlund and Michael I. Schwartzbach. Graph types. In Principles of Programming Languages, POPL'93 ACM, 1993.]]

Digital Library

[29]

Nils Klarlund and Michael I. Schwartzbach. Graphs and decidable transductions based on edge constraints. In Trees in Algebra and Programming, CAAP'94 volume 787 of LNCS 1994.]]

Digital Library

[30]

Nils Klarlund and Michael I. Schwartzbach. A domain-specific language for regular sets of strings and trees. IEEE Transactions On Software Engineering 25(3):378-386, 1999.]]

Digital Library

[31]

Tal Lev-Ami, Thomas Reps, Mooly Sagiv, and Reinhard Wilhelm. Putting static analysis to work for verification: a case study. In International Symposium on Software Testing and Analysis, ISSTA'00 ACM, 2000.]]

Digital Library

[32]

Tal Lev-Ami and Mooly Sagiv. TVLA: A system for implementing static analyses. In Seventh International Static Analysis Symposium, SAS'00 2000.]]

Digital Library

[33]

Albert R. Meyer. Wea monadic second-order theory of successor is not elementary recursive. In R. Parikh, editor, Logic Colloquium, (Proc. Symposium on Logic, Boston, 1972), volume 453 of LNCS pages 132-154, 1975.]]

[34]

Anders Moller. MONA project home page. www.brics.dk/mona]]

[35]

Anders Moller. PALE project home page. www.brics.dk/PALE]]

[36]

Joseph M. Morris. A general axiom of assignment. In Theoretical Foundations of Programming Methodology 1982.]]

[37]

John C. Reynolds. Intuitionistic reasoning about shared mutable data structure. In Millennial Perspectives in Computer Science 2000.]]

[38]

Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm. Parametric shape analysis via 3 valued logic. In Principles of Programming Languages, POPL'99 1999.]]

Digital Library

[39]

Thomas R. Shiple, James H. Kukula, and Rajeev K. Ranjan. A comparison of Presburger engines for EFSM reachability. In Computer Aided Verification, CAV'98 volume 1427 of LNCS, 1998.]]

Digital Library

Cited By

Havlena VHolík LLengál OVojnar T(2021)Automata Terms in a Lazy WSkS Decision ProcedureJournal of Automated Reasoning10.1007/s10817-021-09597-w65:7(971-999)Online publication date: 1-Oct-2021
https://dl.acm.org/doi/10.1007/s10817-021-09597-w
Hruška MHolík L(2021)Towards Efficient Shape Analysis with Tree AutomataNetworked Systems10.1007/978-3-030-91014-3_14(206-214)Online publication date: 2-Dec-2021
https://doi.org/10.1007/978-3-030-91014-3_14
Usman MWang WWang KYelen CDini NKhurshid S(2020)A study of learning likely data structure properties using machine learning modelsInternational Journal on Software Tools for Technology Transfer10.1007/s10009-020-00577-wOnline publication date: 7-Jun-2020
https://doi.org/10.1007/s10009-020-00577-w
Show More Cited By

Index Terms

Recommendations

The pointer assertion logic engine
PLDI '01: Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation

We present a new framework for verifying partial specifications of programs in order to catch type and memory errors and check data structure invariants. Our technique can verify a large class of data structures, namely all those that can be expressed ...
Pointer analysis and separation logic
Tactics for Proving Separation Logic Assertion in Coq Proof Assistant
ICVISP 2019: Proceedings of the 3rd International Conference on Vision, Image and Signal Processing

The verification of the correctness of large programs, particularly operating systems is an unmanageable but important endeavor. we are interested in verifying C programs with formal methods, the logic is separation logic, a Hoare-style program logic. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 36, Issue 5

May 2001

330 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/381694

Issue’s Table of Contents

PLDI '01: Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation
June 2001
331 pages
ISBN:1581134142
DOI:10.1145/378795
Chairmen:
Michael Burke
IBM T.J. Watson Research Center
,
Mary Lou Soffa
Univ. of Pittsburgh

Copyright © 2001 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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 May 2001

Published in SIGPLAN Volume 36, Issue 5

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

220
Total Citations
View Citations
591
Total Downloads

Downloads (Last 12 months)5
Downloads (Last 6 weeks)1

Reflects downloads up to 24 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Havlena VHolík LLengál OVojnar T(2021)Automata Terms in a Lazy WSkS Decision ProcedureJournal of Automated Reasoning10.1007/s10817-021-09597-w65:7(971-999)Online publication date: 1-Oct-2021
https://dl.acm.org/doi/10.1007/s10817-021-09597-w
Hruška MHolík L(2021)Towards Efficient Shape Analysis with Tree AutomataNetworked Systems10.1007/978-3-030-91014-3_14(206-214)Online publication date: 2-Dec-2021
https://doi.org/10.1007/978-3-030-91014-3_14
Usman MWang WWang KYelen CDini NKhurshid S(2020)A study of learning likely data structure properties using machine learning modelsInternational Journal on Software Tools for Technology Transfer10.1007/s10009-020-00577-wOnline publication date: 7-Jun-2020
https://doi.org/10.1007/s10009-020-00577-w
Usman MWang WWang KYelen CDini NKhurshid S(2019)A Study of Learning Data Structure Invariants Using Off-the-shelf ToolsModel Checking Software10.1007/978-3-030-30923-7_13(226-243)Online publication date: 2-Oct-2019
https://doi.org/10.1007/978-3-030-30923-7_13
Havlena VHolík LLengál OVojnar T(2019)Automata Terms in a Lazy WSkS Decision ProcedureAutomated Deduction – CADE 2710.1007/978-3-030-29436-6_18(300-318)Online publication date: 27-Aug-2019
https://dl.acm.org/doi/10.1007/978-3-030-29436-6_18
Qiu XWang Y(2019)A Decidable Logic for Tree Data-Structures with MeasurementsVerification, Model Checking, and Abstract Interpretation10.1007/978-3-030-11245-5_15(318-341)Online publication date: 11-Jan-2019
https://doi.org/10.1007/978-3-030-11245-5_15
Shoham S(2018)Interactive Verification of Distributed Protocols Using Decidable LogicStatic Analysis10.1007/978-3-319-99725-4_7(77-85)Online publication date: 29-Aug-2018
https://doi.org/10.1007/978-3-319-99725-4_7
Stefănescu APark DYuwen SLi YRoşu G(2016)Semantics-based program verifiers for all languagesACM SIGPLAN Notices10.1145/3022671.298402751:10(74-91)Online publication date: 19-Oct-2016
https://dl.acm.org/doi/10.1145/3022671.2984027
Stefănescu APark DYuwen SLi YRoşu GVisser ESmaragdakis Y(2016)Semantics-based program verifiers for all languagesProceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications10.1145/2983990.2984027(74-91)Online publication date: 19-Oct-2016
https://dl.acm.org/doi/10.1145/2983990.2984027
Braione PDenaro GPezzè MZimmermann TCleland-Huang JSu Z(2016)JBSE: a symbolic executor for Java programs with complex heap inputsProceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering10.1145/2950290.2983940(1018-1022)Online publication date: 1-Nov-2016
https://dl.acm.org/doi/10.1145/2950290.2983940
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 Issue’s Table of Contents