Recommendations
Cites work
- scientific article; zbMATH DE number 3714908 (Why is no real title available?)
- scientific article; zbMATH DE number 108539 (Why is no real title available?)
- scientific article; zbMATH DE number 3483531 (Why is no real title available?)
- scientific article; zbMATH DE number 1231564 (Why is no real title available?)
- scientific article; zbMATH DE number 1927580 (Why is no real title available?)
- scientific article; zbMATH DE number 1841809 (Why is no real title available?)
- scientific article; zbMATH DE number 2090840 (Why is no real title available?)
- scientific article; zbMATH DE number 3430097 (Why is no real title available?)
- A hard act to follow
- A structured paging system
- An axiomatic proof technique for parallel programs
- CONCUR 2004 - Concurrency Theory
- Deadlock analysis in networks of communicating processes
- Full abstraction for a shared-variable parallel language
- Local reasoning about a copying garbage collector
- Monitors
- Parallel programming: An axiomatic approach
- Permission accounting in separation logic
- Proofs of Networks of Processes
- Proving Liveness Properties of Concurrent Programs
- Resources, concurrency, and local reasoning
- Separation and information hiding
- The Logic of Bunched Implications
- The essence of parallel Algol.
- The structure of the “THE”-multiprogramming system
- The temporal semantics of concurrent programs
- Verifying properties of parallel programs
Cited in
(84)- Interactive proofs in higher-order concurrent separation logic
- Fairness, resources, and separation
- Unified reasoning about robustness properties of symbolic-heap separation logic
- A formal semantics of nested atomic sections with thread escape
- Verifying a concurrent garbage collector with a rely-guarantee methodology
- Automated theorem proving for assertions in separation logic with all connectives
- RGITL: a temporal logic framework for compositional reasoning about interleaved programs
- Barriers in concurrent separation logic: now with tool support!
- Automatic Parallelization with Separation Logic
- Automata-theoretic semantics of idealized Algol with passive expressions
- Oracle Semantics for Concurrent Separation Logic
- Strict linearizability and abstract atomicity
- An asynchronous soundness theorem for concurrent separation logic
- Precision and the conjunction rule in concurrent separation logic
- \textsc{SecCSL}: security concurrent separation logic
- Separation Logic Contracts for a Java-Like Language with Fork/Join
- Pointer race freedom
- scientific article; zbMATH DE number 47204 (Why is no real title available?)
- On the relation between concurrent separation logic and concurrent Kleene algebra
- Non-preemptive semantics for data-race-free programs
- Stone-type dualities for separation logics
- Permission accounting in separation logic
- A revisionist history of concurrent separation logic
- CONCUR 2004 - Concurrency Theory
- Complexity optimal decision procedure for a propositional dynamic logic with parallel composition
- Elucidating concurrent algorithms via layers of abstraction and reification
- Convolution as a Unifying Concept
- Blaming the client: on data refinement in the presence of pointers
- Fifty years of Hoare's logic
- Syntactic control of interference and concurrent separation logic
- Parallelized sequential composition and hardware weak memory models
- Abstract hidden Markov models: a monadic account of quantitative information flow
- Concurrent separation logic and operational semantics
- Iris from the ground up: a modular foundation for higher-order concurrent separation logic
- Extracting total Amb programs from proofs
- Automated verification of parallel nested DFS
- Concurrent Separation Logic Meets Template Games
- Independence and concurrent separation logic
- A perspective on specifying and verifying concurrent modules
- A separation logic for a promising semantics
- An operational semantics for object-oriented concepts based on the class hierarchy
- Improving thread-modular abstract interpretation
- Verifying programs with logic and extended proof rules: deep embedding vs. shallow embedding
- Partition consistency. A case study in modeling systems with weak memory consistency and proving correctness of their implementations
- Concurrent separation logic for pipelined parallelization
- Barriers in Concurrent Separation Logic
- Shared contract-obedient endpoints
- Separation logic and concurrency
- Parameterized Memory Models and Concurrent Separation Logic
- Trace-based verification of imperative programs with I/O
- Modular reasoning about separation of concurrent data structures
- Separation Logic Semantics for Communicating Processes
- scientific article; zbMATH DE number 7407781 (Why is no real title available?)
- Inter-process buffers in separation logic with rely-guarantee
- Fine-grained concurrency with separation logic
- A calculus and logic of bunched resources and processes
- Higher-order separation logic in Isabelle/HOLCF
- Program logic and equivalence in the presence of garbage collection.
- On locality and the exchange law for concurrent processes
- An algebraic glimpse at bunched implications and separation logic
- Step-indexed Kripke model of separation logic for storable locks
- Revisiting concurrent separation logic
- Formal verification of concurrent programs with Read-write locks
- Communicating state transition systems for fine-grained concurrent resources
- Designing a semantic model for a wide-spectrum language with concurrency
- Separation Logic Tutorial
- A discrete geometric model of concurrent program execution
- A fine-grained semantics for arrays and pointers under weak memory models
- A grainless semantics for parallel programs with shared mutable data
- Variables as resource for shared-memory programs: semantics and soundness
- Completeness for a first-order abstract separation logic
- A separation logic for refining concurrent objects
- A first-order logic with frames
- A predicate transformer for choreographies. Computing preconditions in choreographic programming
- Separation and information hiding
- A resource analysis of the \(\pi\)-calculus
- Local Reasoning for Storable Locks and Threads
- A Formalisation of Smallfoot in HOL
- Reasoning about block-based cloud storage systems via separation logic
- Ownership guided C to Rust translation
- Practical abstractions for automated verification of message passing concurrency
- Granularity and concurrent separation logic
- Type soundness and race freedom for Mezzo
- Compositional reasoning
This page was built for publication: A semantics for concurrent separation logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q879367)
