Checking interference with fractional permissions

DOI10.1007/3-540-44898-5_4MaRDI QIDQ4813391zbMATH OpenFDO

Authors John Tang Boyland

Publication date 13 August 2004

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2694/26940055.htm

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Permission accounting in separation logic
• Noninterference for concurrent programs
• Polymorphic Fractional Capabilities
• Noninterference for concurrent programs and thread systems
• On interference abstractions

Cited in

(44)

• A perspective on specifying and verifying concurrent modules
• A formal C memory model for separation logic
• Stepwise refinement of heap-manipulating code in Chalice
• Formal verification of parallel prefix sum and stream compaction algorithms in CUDA
• Automated verification of the parallel Bellman-Ford algorithm
• Revisiting concurrent separation logic
• Automata-theoretic semantics of idealized Algol with passive expressions
• Modular termination verification for non-blocking concurrency
• Automatic inference of access permissions
• A type system for borrowing permissions
• Temporary read-only permissions for separation logic
• Tackling real-life relaxed concurrency with FSL++
• The essence of higher-order concurrent separation logic
• The relationship between separation logic and implicit dynamic frames
• Syntactic control of interference and concurrent separation logic
• Polymorphic Fractional Capabilities
• Automatic Parallelization and Optimization of Programs by Proof Rewriting
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• A concurrent constraint programming interpretation of access permissions
• Automated verification of parallel nested DFS
• Concise read-only specifications for better synthesis of programs with pointers
• RustHorn: CHC-based verification for Rust programs
• ConSORT: context- and flow-sensitive ownership refinement types for imperative programs
• On Symbolic Heaps Modulo Permission Theories
• Verification of concurrent systems with VerCors
• Reasoning about separation using abstraction and reification
• The dynamic frames theory
• Separation Logic Contracts for a Java-Like Language with Fork/Join
• A revisionist history of concurrent separation logic
• A resource analysis of the \(\pi\)-calculus
• Concurrent separation logic and operational semantics
• Steps in modular specifications for concurrent modules (invited tutorial paper)
• Concise outlines for a complex logic: a proof outline checker for TaDA
• Linearity and uniqueness: an entente cordiale
• Sound Automation of Magic Wands
• Practical abstractions for automated verification of message passing concurrency
• A generalised union of rely-guarantee and separation logic using permission algebras
• Preserving provability over GPU program optimizations with annotation-aware transformations
• Unbounded Separation Logic
• A Restricted Definition of the Magic Wand to Soundly Combine Fractions of a Wand
• Fine-grained concurrency with separation logic
• A semantics for concurrent separation logic
• Resources, concurrency, and local reasoning
• Balancing expressiveness in formal approaches to concurrency

This page was built for publication: Checking interference with fractional permissions

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