Verifying properties of well-founded linked lists
From MaRDI portal
Publication:5348918
DOI10.1145/1111037.1111048zbMath1369.68143OpenAlexW2123828382MaRDI QIDQ5348918
Shuvendu K. Lahiri, Shaz Qadeer
Publication date: 21 August 2017
Published in: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/1111037.1111048
automated theorem provingfirst-order axiomatizationdecision procedureheap abstractionwell-founded linked lists
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (10)
A logic of reachable patterns in linked data-structures ⋮ Verifying Heap-Manipulating Programs in an SMT Framework ⋮ Monotonic Abstraction for Programs with Dynamic Memory Heaps ⋮ Automated verification of shape, size and bag properties via user-defined predicates in separation logic ⋮ Enforcing Structural Invariants Using Dynamic Frames ⋮ Bounded Quantifier Instantiation for Checking Inductive Invariants ⋮ Matching Logic: An Alternative to Hoare/Floyd Logic ⋮ An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures ⋮ A shape graph logic and a shape system ⋮ Automata-Based Termination Proofs
This page was built for publication: Verifying properties of well-founded linked lists
