Verifying properties of well-founded linked lists
From MaRDI portal
Publication:5348918
DOI10.1145/1111037.1111048zbMath1369.68143MaRDI 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 proving; first-order axiomatization; decision procedure; heap abstraction; well-founded linked lists
68P05: Data structures
68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Related Items
An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures, Automated verification of shape, size and bag properties via user-defined predicates in separation logic, A shape graph logic and a shape system, A logic of reachable patterns in linked data-structures, Enforcing Structural Invariants Using Dynamic Frames, Matching Logic: An Alternative to Hoare/Floyd Logic, Bounded Quantifier Instantiation for Checking Inductive Invariants, Verifying Heap-Manipulating Programs in an SMT Framework, Monotonic Abstraction for Programs with Dynamic Memory Heaps, Automata-Based Termination Proofs
