dk.brics.automaton  |  dk.brics.grammar  |  dk.brics.schematools
TAJS  |  Java String Analyzer  |  XSLT Validator  |  ServletValidator  |  XSugar  |  Xact  |  JWIG
MONA  |  PALE

PALE - the Pointer Assertion Logic Engine

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
a counterexample produced by PALE PALE is implemented by Anders Møller at Aarhus University.