The Pointer Assertion Logic Engine

TY - GEN

T1 - The Pointer Assertion Logic Engine

AU - Møller, Anders

AU - Schwartzbach, Michael Ignatieff

N1 - Conference code: 15

PY - 2001

Y1 - 2001

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

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

U2 - 10.1145/381694.378851

DO - 10.1145/381694.378851

M3 - Article in proceedings

SN - 1-58113-414-2

VL - 36(5)

SP - 221

EP - 231

BT - Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation

A2 - Sofia, Mary Lou

PB - Association for Computing Machinery

T2 - Conference on Programming Language Design and Implementation. PLDI '01

Y2 - 20 June 2001 through 22 June 2001

ER -