The pointer assertion logic engine

By Anders Møller, Michael I. Schwartzbach. ACM-SIGPLAN Symposium on Programming Language Design and Implementation, 2000

295 citations recorded by the source corpus.

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.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Software

View Paper: https://www.semanticscholar.org/paper/1442c43a70e47a004c62796e510cccecc4898562

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

In Software

Citations in the corpus

Smallfoot: Modular Automatic Assertion Checking with Separation Logic (2005, background): “The most closely related works to Smallfoot are the Pointer Assertion Logic Engine [28] and Alias Types [39] and its relatives (e.”
Korat: automated testing based on Java predicates (2002, background): “While TVLA and PALE are primarily intraprocedural, Role Analysis [19] supports compositional interprocedural analysis and veri.es similar properties.”
Symbolic Execution with Separation Logic (2005, background): “The notion of symbolic execution presented in this paper is, in a general sense, similar in spirit to what one obtains in Shape Analysis or PALE [14, 7].”
Software model checking (2009, unknown): “The Pale tool is built on top of MSOL and enables reasoning about tree-like data structures [Møller and Schwartzbach 2001].”
Test input generation with java PathFinder (2004, background): “The pointer assertion logic engine (PALE) [36] can verify a large class of data structures that can be represented by a spanning tree backbone, with possibly additional pointers.”
Generalized Symbolic Execution for Model Checking and Testing (2003, background): “The pointer assertion logic engine (PALE) [15] can verify a large class of data structures that can be represented by a spanning tree backbone, with possibly additional pointers that do not add extra information.”
TestEra: a novel framework for automated testing of Java programs (2001, methodology): “This is evident from the fact that the fourth property of red-black trees is not expressible in the logics used in [4, 22].”
Ownership types for safe programming: preventing data races and deadlocks (2002, methodology): “Shape Analysis: Systems such as TVLA [42], PALE [39], and Roles [30] specify the shape of a local object graph in more detail than ownership types.”