Verifying properties of well-founded linked lists

DOI10.1145/1111037.1111048MaRDI QIDQ5348918zbMATH OpenOpenAlexFDO

Authors 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

zbMATH Keywords

automated theorem provingdecision procedurefirst-order axiomatizationheap abstractionwell-founded linked lists

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Data structures (68P05)

Recommendations

• Predicate abstraction for linked data structures
• Programs with Lists Are Counter Automata
• Verification, Model Checking, and Abstract Interpretation
• Programs with lists are counter automata
• Propositional reasoning about safety and termination of heap-manipulating programs

Cited in

(18)

• A logic of reachable patterns in linked data-structures
• Predicate abstraction for linked data structures
• Propositional reasoning about safety and termination of heap-manipulating programs
• 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
• Refinement-Based Verification for Possibly-Cyclic Lists
• Automata-Based Termination Proofs
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• Verification of multi-linked heaps
• Programs with lists are counter automata
• An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures
• On Flat Programs with Lists
• Proving Properties about Lists Using Containers
• Verification, Model Checking, and Abstract Interpretation
• A shape graph logic and a shape system

This page was built for publication: Verifying properties of well-founded linked lists

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5348918)