Simulating Reachability using First-Order Logic with Applications to Verification of Linked Data Structures

Abstract

This paper shows how to harness existing theorem provers for first-order logic to automatically verify safety properties of imperative programs that perform dynamic storage allocation and destructive updating of pointer-valued structure fields. One of the main obstacles is specifying and proving the (absence) of reachability properties among dynamically allocated cells. The main technical contributions are methods for simulating reachability in a conservative way using first-order formulasthe formulas describe a superset of the set of program states that can actually arise. These methods are employed for semi-automatic program verification (i.e., using programmer-supplied loop invariants) on programs such as mark-and-sweep garbage collection and destructive reversal of a singly linked list. (The mark-and-sweep example has been previously reported as being beyond the capabilities of ESC/Java.)

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 2009
Accession Number
AD1004498

Entities

People

  • G. Yorsh
  • M. Sagiv
  • N. Immerman
  • Shivani Srivastava
  • T. Lev-ami
  • T. Reps

Organizations

  • University of Massachusetts Amherst

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Abstracts
  • Algorithms
  • Computer Programming
  • Iterations
  • Language
  • Lists (Data Structures)
  • Models
  • Notation
  • Programming Languages
  • Reasoning
  • Semantic Models
  • Simulations
  • Specifications
  • Transformers
  • Trees (Data Structures)
  • Verification
  • Vocabulary

Readers

  • Mathematical Modeling and Probability Theory.
  • Parallel and Distributed Computing.