Types, bytes, and separation logic
From MaRDI portal
Publication:3189788
DOI10.1145/1190216.1190234zbMath1295.68094OpenAlexW4232666937MaRDI QIDQ3189788
Harvey Tuch, Michael Norrish, Gerwin Klein
Publication date: 12 September 2014
Published in: Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/1190216.1190234
Theory of programming languages (68N15) Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Formal verification of C systems code. Structured types, separation logic and theorem proving ⋮ Formal memory models for the verification of low-level operating-system code ⋮ Types, Maps and Separation Logic ⋮ Practical Tactics for Separation Logic ⋮ A Formalisation of Smallfoot in HOL ⋮ HOL-Boogie -- an interactive prover-backend for the verifying C compiler ⋮ Aliasing Restrictions of C11 Formalized in Coq ⋮ A Concrete Memory Model for CompCert ⋮ A formal C memory model for separation logic ⋮ Function extraction ⋮ Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning ⋮ The Isabelle Framework ⋮ Imperative Functional Programming with Isabelle/HOL ⋮ Secure Microkernels, State Monads and Scalable Refinement ⋮ Lightweight Separation ⋮ Formalizing non-interference for a simple bytecode language in Coq ⋮ A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data ⋮ Formal verification of a C-like memory model and its uses for verifying program transformations ⋮ From a Proven Correct Microkernel to Trustworthy Large Systems ⋮ A Machine-Checked Framework for Relational Separation Logic ⋮ A Framework for the Automatic Formal Verification of Refinement from Cogent to C ⋮ Operating system verification---an overview ⋮ Separation Logic Tutorial ⋮ Cogent: uniqueness types and certifying compilation
Uses Software
