Lightweight Separation

DOI10.1007/978-3-540-71067-7_18zbMath1165.68458OpenAlexW2913100775MaRDI QIDQ3543659

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

Related Items (2)

Reasoning about memory layouts ⋮ A Machine-Checked Framework for Relational Separation Logic

Uses Software

• Isabelle
• HIP
• Smallfoot

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Formal verification of C systems code. Structured types, separation logic and theorem proving
• Axiomatic approach to side effects and general jumps
• Isabelle. A generic theorem prover
• Proving pointer programs in higher-order logic
• Types, bytes, and separation logic
• Separation Logic for Small-Step cminor
• Interprocedural Shape Analysis with Separated Heap Abstractions
• Computer Science Logic
• Shape Analysis for Composite Data Structures
• Automated Verification of Shape and Size Properties Via Separation Logic
• Programming Languages and Systems
• Tools and Algorithms for the Construction and Analysis of Systems

This page was built for publication: Lightweight Separation