Simulating reachability using first-order logic with applications to verification of linked data structures

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

30 Citations (Scopus)

Abstract

This paper shows how lo harness exisling Iheorcm provers for firslorder logic lo automatically verify safely properlies of imperative programs lhal 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 formulas-the 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.)

Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages99-115
Number of pages17
StatePublished - Dec 1 2005
Externally publishedYes
Event20th International Conference on Automated Deduction, CADE-20 - Tallinn, Estonia
Duration: Jul 22 2005Jul 27 2005

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3632 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other20th International Conference on Automated Deduction, CADE-20
CountryEstonia
CityTallinn
Period7/22/057/27/05

Fingerprint

Linked Data
First-order Logic
Reachability
Data structures
Data Structures
Sweep
Automatic Verification
Garbage Collection
Program Verification
Reversal
Java
Updating
Logic
Verify
First-order
Invariant
Cell

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Lev-Ami, T., Immerman, N., Reps, T., Sagiv, M., Srivastava, S., & Yorsh, G. (2005). Simulating reachability using first-order logic with applications to verification of linked data structures. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 99-115). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3632 LNAI).

Simulating reachability using first-order logic with applications to verification of linked data structures. / Lev-Ami, T.; Immerman, N.; Reps, T.; Sagiv, M.; Srivastava, Siddharth; Yorsh, G.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2005. p. 99-115 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3632 LNAI).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Lev-Ami, T, Immerman, N, Reps, T, Sagiv, M, Srivastava, S & Yorsh, G 2005, Simulating reachability using first-order logic with applications to verification of linked data structures. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 3632 LNAI, pp. 99-115, 20th International Conference on Automated Deduction, CADE-20, Tallinn, Estonia, 7/22/05.
Lev-Ami T, Immerman N, Reps T, Sagiv M, Srivastava S, Yorsh G. Simulating reachability using first-order logic with applications to verification of linked data structures. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2005. p. 99-115. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Lev-Ami, T. ; Immerman, N. ; Reps, T. ; Sagiv, M. ; Srivastava, Siddharth ; Yorsh, G. / Simulating reachability using first-order logic with applications to verification of linked data structures. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2005. pp. 99-115 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{dd3c87796b3c40b9b3d4d4c04e670c5a,
title = "Simulating reachability using first-order logic with applications to verification of linked data structures",
abstract = "This paper shows how lo harness exisling Iheorcm provers for firslorder logic lo automatically verify safely properlies of imperative programs lhal 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 formulas-the 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.)",
author = "T. Lev-Ami and N. Immerman and T. Reps and M. Sagiv and Siddharth Srivastava and G. Yorsh",
year = "2005",
month = "12",
day = "1",
language = "English (US)",
isbn = "3540280057",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "99--115",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

TY - GEN

T1 - Simulating reachability using first-order logic with applications to verification of linked data structures

AU - Lev-Ami, T.

AU - Immerman, N.

AU - Reps, T.

AU - Sagiv, M.

AU - Srivastava, Siddharth

AU - Yorsh, G.

PY - 2005/12/1

Y1 - 2005/12/1

N2 - This paper shows how lo harness exisling Iheorcm provers for firslorder logic lo automatically verify safely properlies of imperative programs lhal 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 formulas-the 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.)

AB - This paper shows how lo harness exisling Iheorcm provers for firslorder logic lo automatically verify safely properlies of imperative programs lhal 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 formulas-the 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.)

UR - http://www.scopus.com/inward/record.url?scp=26944445043&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=26944445043&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:26944445043

SN - 3540280057

SN - 9783540280057

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 99

EP - 115

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

ER -