Temporary Read-Only Permissions for Separation Logic

DOI10.1007/978-3-662-54434-1_10zbMath1485.68056OpenAlexW2585684928MaRDI QIDQ2988642

François Pottier, Arthur Charguéraud

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)

Related Items (3)

Concise Read-Only Specifications for Better Synthesis of Programs with Pointers ⋮ Characteristic formulae for liveness properties of non-terminating CakeML programs ⋮ A relational shape abstract domain

Uses Software

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

Cites Work

• Unnamed Item
• Resources, concurrency, and local reasoning
• Charge!
• Views
• High-level separation logic for low-level code
• A type system for borrowing permissions
• Verified Software Toolchain
• Local Reasoning for Storable Locks and Threads
• A Basis for Verifying Multi-threaded Programs
• Program verification through characteristic formulae
• Characteristic formulae for the verification of imperative programs
• Permission accounting in separation logic
• Connecting effects and uniqueness with adoption
• Oracle Semantics for Concurrent Separation Logic

This page was built for publication: Temporary Read-Only Permissions for Separation Logic