Verify heaps via unified model checking
From MaRDI portal
Publication:1986561
DOI10.1016/j.tcs.2017.09.025zbMath1464.68209OpenAlexW2796100766MaRDI QIDQ1986561
Xu Lu, Zhenhua Duan, Cong Tian, Hongwei David Du
Publication date: 8 April 2020
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2017.09.025
Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Data structures (68P05) Temporal logic (03B44) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
An adaptation-complete proof system for local reasoning about cloud storage systems ⋮ Reasoning about block-based cloud storage systems via separation logic
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- On the almighty wand
- Model checking dynamic memory allocation in operating systems
- Framed temporal logic programming
- A decision procedure for propositional projection temporal logic with infinite models
- Verifying Temporal Heap Properties Specified via Evolution Logic
- Propositional Projection Temporal Logic, B $\ddot{u}$ chi Automata and ω-Regular Expressions
- Safety and Liveness in Concurrent Pointer Programs
- Abstract Regular Tree Model Checking of Complex Dynamic Data Structures
- Complexity of propositional projection temporal logic with star
- Simulating reachability using first-order logic with applications to verification of linked data structures
- BI as an assertion language for mutable data structures
- Compositional Shape Analysis by Means of Bi-Abduction
- Programming Languages and Systems
- Foundations of Software Science and Computational Structures
- Verification, Model Checking, and Abstract Interpretation
- Tools and Algorithms for the Construction and Analysis of Systems
