Skip to main content

Verifying Reachability Invariants of Linked Structures

DOI 10.1145/567067.567073 dblp BibTeX

Abstract

The paper introduces a reachability predicate for linear lists, develops the elementary axiomatic theory of the predicate, and illustrates its application to program verification with a formal proof of correctness for a short program that traverses and splices linear lists.

Related papers

Verifying properties of well-founded linked lists POPL 2006
Effectively-Propositional Reasoning about Reachability in Linked Data Structures CAV 2013
Automatic Verification of Pointer Programs using Monadic Second-Order Logic PLDI 1997
Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking TACAS 2005
Modular reasoning about heap paths via effectively propositional formulas POPL 2014
Verification of semantic commutativity conditions and inverse operations on linked data structures PLDI 2011
Verifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic PLDI 2025
Verified Lock-Free Session Channels with Linking OOPSLA 2024