Temporary read-only permissions for separation logic

DOI10.1007/978-3-662-54434-1_10MaRDI QIDQ2988642zbMATH OpenOpenAlexFDO

Authors Arthur Charguéraud, François Pottier

Publication date 19 May 2017

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/hal-01408657v2/file/readonlysep.pdf

Mathematics Subject Classification ID

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

Recommendations

• Permission accounting in separation logic
• Syntactic control of interference and concurrent separation logic
• Reasoning over permissions regions in concurrent separation logic
• A revisionist history of concurrent separation logic
• Separation logic and concurrency

Cites work

• A Basis for Verifying Multi-threaded Programs
• A type system for borrowing permissions
• Characteristic formulae for the verification of imperative programs
• Charge! A framework for higher-order separation logic in Coq
• Connecting effects and uniqueness with adoption
• High-level separation logic for low-level code
• scientific article; zbMATH DE number 2090840 (Why is no real title available?)
• Local Reasoning for Storable Locks and Threads
• Oracle Semantics for Concurrent Separation Logic
• Permission accounting in separation logic
• Program verification through characteristic formulae
• Resources, concurrency, and local reasoning
• Verified software toolchain (invited talk)
• Views, compositional reasoning for concurrent programs

Cited in

(3)

• A relational shape abstract domain
• Concise read-only specifications for better synthesis of programs with pointers
• Characteristic formulae for liveness properties of non-terminating CakeML programs

Describes a project that uses

Uses Software

• Coq
• Toolchain
• Smallfoot
• jStar
• Mezzo
• Infer
• Charge!
• Rust

This page was built for publication: Temporary read-only permissions for separation logic

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