A Marriage of Rely/Guarantee and Separation Logic
From MaRDI portal
(Redirected from Publication:3525642)
Recommendations
Cited in
(50)- A temporal programming model with atomic blocks based on projection temporal logic
- Proof tactics for assertions in separation logic
- Verifying a concurrent garbage collector using a rely-guarantee methodology
- Weak updates and separation logic
- Decision problems in a logic for reasoning about reconfigurable distributed systems
- RGITL: a temporal logic framework for compositional reasoning about interleaved programs
- Verifying a concurrent garbage collector with a rely-guarantee methodology
- Program equivalence in linear contexts
- On the relation between concurrent separation logic and concurrent Kleene algebra
- Revisiting concurrent separation logic
- Compositional verification of a communication protocol for a remotely operated aircraft
- Effect algebras, Girard quantales and complementation in separation logic
- Towards a thread-local proof technique for starvation freedom
- Certificates and Separation Logic
- A higher-order logic for concurrent termination-preserving refinement
- Abstract specifications for concurrent maps
- Granularity and concurrent separation logic
- A machine-checked framework for relational separation logic
- Completeness for a first-order abstract separation logic
- CSimpl: a rely-guarantee-based framework for verifying concurrent programs
- Automated theorem proving for assertions in separation logic with all connectives
- Formal verification of concurrent programs with Read-write locks
- Splitting Atoms with Rely/Guarantee Conditions Coupled with Data Reification
- Deny-Guarantee Reasoning
- Separation logics and modalities: a survey
- Iris from the ground up: a modular foundation for higher-order concurrent separation logic
- Explanation of two non-blocking shared-variable communication algorithms
- A dynamic logic for deductive verification of multi-threaded programs
- Ott: Effective tool support for the working semanticist
- Local rely-guarantee reasoning
- Reasoning about separation using abstraction and reification
- Expressive completeness of separation logic with two variables and no separating conjunction
- Proving linearizability with temporal logic
- Algebraic separation logic
- Concurrent separation logic and operational semantics
- Automatically verifying temporal properties of pointer programs with cyclic proof
- Inter-process buffers in separation logic with rely-guarantee
- Rely-guarantee reasoning for causally consistent shared memory
- Specifying and reasoning about shared-variable concurrency
- Practical abstractions for automated verification of message passing concurrency
- Extending rely-guarantee thinking to handle real-time scheduling
- Compositional reasoning for non-multicopy atomic architectures
- A generalised union of rely-guarantee and separation logic using permission algebras
- A general approach to under-approximate reasoning about concurrent programs
- Locksynth: deriving synchronization code for concurrent data structures with ASP
- A compositional theory of linearizability
- Fine-grained concurrency with separation logic
- Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper)
- Certifying low-level programs with hardware interrupts and preemptive threads
- Balancing expressiveness in formal approaches to concurrency
This page was built for publication: A Marriage of Rely/Guarantee and Separation Logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3525642)
