Automated Verification of Shape and Size Properties Via Separation Logic
From MaRDI portal
Publication:5452612
DOI10.1007/978-3-540-69738-1_18zbMath1132.68477OpenAlexW1567479568MaRDI QIDQ5452612
Shengchao Qin, Cristina David, Wei-Ngan Chin, Huu Hai Nguyen
Publication date: 4 April 2008
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: http://dro.dur.ac.uk/6213/1/6213.pdf
Specification and verification (program logics, model checking, etc.) (68Q60) Data structures (68P05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (16)
Completeness for recursive procedures in separation logic ⋮ Crowfoot: A Verifier for Higher-Order Store Programs ⋮ Automata-based verification of programs with tree updates ⋮ Verifying pointer safety for programs with unknown calls ⋮ Automated mutual induction proof in separation logic ⋮ Completeness and expressiveness of pointer program verification by separation logic ⋮ Linear Arithmetic with Stars ⋮ Automated verification of shape, size and bag properties via user-defined predicates in separation logic ⋮ Forest automata for verification of heap manipulation ⋮ Lightweight Separation ⋮ Automated Cyclic Entailment Proofs in Separation Logic ⋮ Decision Procedures for Multisets with Cardinality Constraints ⋮ Beyond Shapes: Lists with Ordered Data ⋮ Efficient bounded model checking of heap-manipulating programs using tight field bounds ⋮ A relational shape abstract domain ⋮ Invariants Synthesis over a Combined Domain for Automated Program Verification
Uses Software
This page was built for publication: Automated Verification of Shape and Size Properties Via Separation Logic
