Types, bytes, and separation logic

DOI10.1145/1190216.1190234MaRDI QIDQ3189788zbMATH OpenOpenAlexFDO

Authors Harvey Tuch, Gerwin Klein, Michael Norrish

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

zbMATH Keywords

Cinteractive theorem provingseparation logic

Mathematics Subject Classification ID

Logic in computer science (03B70) Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Types, Maps and Separation Logic
• Formal verification of C systems code. Structured types, separation logic and theorem proving
• Computer Science Logic
• A formal C memory model for separation logic
• Mechanised Separation Algebra

Cited in

(38)

• Operating system verification---an overview
• Formally verifying exceptions for low-level code with separation logic
• A formal C memory model for separation logic
• A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data
• The meaning of memory safety
• HOL-Boogie -- an interactive prover-backend for the verifying C compiler
• A framework for the automatic formal verification of refinement from \textsc{Cogent} to C
• Aliasing restrictions of C11 formalized in Coq
• A concrete memory model for CompCert
• From a proven correct microkernel to trustworthy large systems
• A machine-checked framework for relational separation logic
• Types, Maps and Separation Logic
• Practical Tactics for Separation Logic
• A Formalisation of Smallfoot in HOL
• Separation Logic for Small-Step cminor
• The Isabelle Framework
• Imperative Functional Programming with Isabelle/HOL
• Secure Microkernels, State Monads and Scalable Refinement
• Lightweight Separation
• Abstracting Allocation
• Function extraction
• Simpl
• Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning
• Linear capabilities for fully abstract compilation of separation-logic-verified code
• Cogent: uniqueness types and certifying compilation
• Low-level liquid types
• Frame rules from answer types for code pointers
• A Unified Memory Model for Pointers
• Higher-order separation logic in Isabelle/HOLCF
• Separation Logic Tutorial
• Reasoning about memory layouts
• A verified specification of TLSF memory management allocator using state monads
• A rely-guarantee-based simulation for cooperative semantics
• Defining and preserving more C behaviors: verified compilation using a concrete memory model
• 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
• Formalizing non-interference for a simple bytecode language in Coq
• Formal verification of a C-like memory model and its uses for verifying program transformations

Describes a project that uses

Uses Software

• Isabelle/HOL

This page was built for publication: Types, bytes, and separation logic

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