Abstracting Allocation

DOI10.1007/11874683_12MaRDI QIDQ3613337zbMATH OpenOpenAlexFDO

Authors Nick Benton

Publication date 12 March 2009

Published in Computer Science Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11874683_12

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Recommendations

• Types, bytes, and separation logic
• Computer Science Logic
• scientific article; zbMATH DE number 1696614
• Types, Maps and Separation Logic
• Formal verification of C systems code. Structured types, separation logic and theorem proving

Cited in

(9)

• Specification patterns for reasoning about recursion through the store
• scientific article; zbMATH DE number 1696614 (Why is no real title available?)
• Staged allocation: a compositional technique for specifying and implementing procedure calling conventions
• Abstraction and subsumption in modular verification of C programs
• Modular verification of procedure equivalence in the presence of memory allocation
• A logical approach to type soundness
• Blaming the client: on data refinement in the presence of pointers
• Hoare-style logic for unstructured programs
• Formally verifying exceptions for low-level code with separation logic

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Abstracting Allocation

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