Pointer Assertion Logic

Pointer Assertion Logic is a notation for expressing assertions about the heap structure of imperative languages. It allows programmers to specify pre- and post-conditions of procedures, loop invariants, and other assertions in Weak Monadic Second-order Logic of Graph Types - a logic that allows many common data structures to be expressed. The logic is decidable, meaning that the assertions can be verified automatically. The main target applications are safety critical data type algorithms.

PALE - the Pointer Assertion Logic Engine - is a complete implementation of the technique, based on the MONA tool. It analyses an annotated program and reports null-pointer dereferences, memory leaks, and violations of assertions and graph type errors.

Latest release: version 1.0-9

Read the paper: The Pointer Assertion Logic Engine [ abstract | PDF | BibTeX ] (in Proc. PLDI'01)
Download PALE (and MONA).
Try the example programs.
See the grammar for the PALE syntax and a technical description of the encoding of PALE in MONA.
See also the MONA project.

PALE is implemented by Anders Møller at Aarhus University.