The Pointer Assertion Logic Engine

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

  • Department of Computer Science

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.

Original languageEnglish
Title of host publicationProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation
EditorsMary Lou Sofia
Number of pages10
PublisherAssociation for Computing Machinery
Publication year2001
ISBN (print)1-58113-414-2
Publication statusPublished - 2001
EventConference on Programming Language Design and Implementation. PLDI '01 - Snowbird, Utah, United States
Duration: 20 Jun 200122 Jun 2001
Conference number: 15


ConferenceConference on Programming Language Design and Implementation. PLDI '01
LandUnited States
BySnowbird, Utah

See relations at Aarhus University Citationformats

ID: 283014