The Pointer Assertion Logic Engine

Anders Møller, Michael Ignatieff Schwartzbach

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

    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.

    Original languageEnglish
    Title of host publicationProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation
    EditorsMary Lou Sofia
    Number of pages10
    Volume36(5)
    PublisherAssociation for Computing Machinery
    Publication date2001
    Pages221-231
    ISBN (Print)1-58113-414-2
    DOIs
    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

    Conference

    ConferenceConference on Programming Language Design and Implementation. PLDI '01
    Number15
    Country/TerritoryUnited States
    CitySnowbird, Utah
    Period20/06/200122/06/2001

    Fingerprint

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

    Cite this