Using Unified Model Checking to Verify Heaps

DOI10.1007/978-3-319-48749-6_55zbMath1483.68199OpenAlexW2545959453MaRDI QIDQ2958361

Xu Lu, Zhenhua Duan, Cong Tian

Publication date: 1 February 2017

Published in: Combinatorial Optimization and Applications (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-48749-6_55

zbMATH Keywords

model checkingseparation logicMSVLheap verificationPPTL

Mathematics Subject Classification ID

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)

Cites Work

• Model checking dynamic memory allocation in operating systems
• Framed temporal logic programming
• Verifying Temporal Heap Properties Specified via Evolution Logic
• Safety and Liveness in Concurrent Pointer Programs
• Compositional Shape Analysis by Means of Bi-Abduction
• Programming Languages and Systems

This page was built for publication: Using Unified Model Checking to Verify Heaps