Automated Verification of Shape and Size Properties Via Separation Logic

DOI10.1007/978-3-540-69738-1_18MaRDI QIDQ5452612zbMATH OpenOpenAlexFDO

Authors Huu Hai Nguyen, Cristina David, Shengchao Qin, Wei-Ngan Chin

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

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Data structures (68P05) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• Programming Languages and Systems
• A shape graph logic and a shape system
• Automated verification of recursive programs with pointers
• Verifying pointer safety for programs with unknown calls

Cited in

(23)

• Loop invariant synthesis in a combined abstract domain
• Efficient bounded model checking of heap-manipulating programs using tight field bounds
• A relational shape abstract domain
• Automated mutual induction proof in separation logic
• Completeness and expressiveness of pointer program verification by separation logic
• Forest automata for verification of heap manipulation
• Completeness for recursive procedures in separation logic
• Invariants synthesis over a combined domain for automated program verification
• Crowfoot: A Verifier for Higher-Order Store Programs
• Automated verification of recursive programs with pointers
• On automated lemma generation for separation logic with inductive definitions
• Linear Arithmetic with Stars
• Enhancing Program Verification with Lemmas
• Lightweight Separation
• Beyond Shapes: Lists with Ordered Data
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• Survey of research on program verification via separation logic
• Automated cyclic entailment proofs in separation logic
• Towards Abstraction-Based Verification of Shape Calculus
• Decision Procedures for Multisets with Cardinality Constraints
• Verifying pointer safety for programs with unknown calls
• A shape graph logic and a shape system
• Automata-based verification of programs with tree updates

Describes a project that uses

Uses Software

• HIP
• Smallfoot

This page was built for publication: Automated Verification of Shape and Size Properties Via Separation Logic

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