Accession Number:

AD1004498

Title:

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

Descriptive Note:

Journal Article

Corporate Author:

MASSACHUSETTS UNIV AMHERST AMHERST United States

Personal Author(s):

• Lev-Ami,T.
• Immerman,N.
• Reps,T.
• Sagiv,M.
• Srivastava,S.
• Yorsh,G.

Report Date:

2009-01-01

Pagination or Media Count:

15.0

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 ESCJava.

Descriptors:

• LOGIC
• theorems
• verification
• reasoning
• semantic models
• language

Subject Categories:

Distribution Statement:

APPROVED FOR PUBLIC RELEASE