Lightweight Separation

DOI10.1007/978-3-540-71067-7_18MaRDI QIDQ3543659zbMATH OpenOpenAlexFDO

Authors Holger Gast

Publication date 4 December 2008

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-71067-7_18

Mathematics Subject Classification ID

Recommendations

• Automatic Parallelization with Separation Logic
• Separation logic modulo theories
• Weak updates and separation logic
• Separation logic adapted for proofs by rewriting
• Algebraic separation logic

Cites work

• Automated Verification of Shape and Size Properties Via Separation Logic
• Axiomatic approach to side effects and general jumps
• Computer Science Logic
• Formal verification of C systems code. Structured types, separation logic and theorem proving
• scientific article; zbMATH DE number 1612488 (Why is no real title available?)
• scientific article; zbMATH DE number 2081098 (Why is no real title available?)
• scientific article; zbMATH DE number 1841809 (Why is no real title available?)
• scientific article; zbMATH DE number 2090132 (Why is no real title available?)
• scientific article; zbMATH DE number 3410595 (Why is no real title available?)
• Interprocedural Shape Analysis with Separated Heap Abstractions
• Isabelle. A generic theorem prover
• Programming Languages and Systems
• Proving pointer programs in higher-order logic
• Separation Logic for Small-Step cminor
• Shape Analysis for Composite Data Structures
• Tools and Algorithms for the Construction and Analysis of Systems
• Types, bytes, and separation logic

Cited in

(4)

• A machine-checked framework for relational separation logic
• Lightweight fusion by fixed point promotion
• scientific article; zbMATH DE number 1440560 (Why is no real title available?)
• Reasoning about memory layouts

Describes a project that uses

Uses Software

• Isabelle
• HIP
• Smallfoot

This page was built for publication: Lightweight Separation

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