The Pointer Assertion Logic Engine

Anders Møller, Michael Ignatieff Schwartzbach

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


    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 date2001
    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
    Country/TerritoryUnited States
    CitySnowbird, Utah


    Dive into the research topics of 'The Pointer Assertion Logic Engine'. Together they form a unique fingerprint.

    Cite this