PALE stands for Pointer Assertion Logic Engine.
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.
GCC is required to compile the source.
It has been tested under Linux, Solaris, and Cygwin/Windows.
Find us on Google+
