The pointer assertion logic engine
| Autor: | Michael I. Schwartzbach, Anders Møller |
|---|---|
| Rok vydání: | 2001 |
| Předmět: |
Shape analysis (program analysis)
Theoretical computer science Correctness Computer science Programming language Subroutine Assertion Monad (functional programming) Data structure Notation computer.software_genre Computer Graphics and Computer-Aided Design Operational semantics Decidability Pointer (computer programming) Graph (abstract data type) computer Software Counterexample |
| Zdroj: | PLDI BRICS Report Series; No 39 (2000): RS-39 The Pointer Assertion Logic Engine BRICS Report Series; Nr. 39 (2000): RS-39 The Pointer Assertion Logic Engine |
| ISSN: | 1558-1160 0362-1340 1601-5355 0909-0878 |
| DOI: | 10.1145/381694.378851 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|