Cites work
- scientific article; zbMATH DE number 1629948 (Why is no real title available?)
- scientific article; zbMATH DE number 1728235 (Why is no real title available?)
- scientific article; zbMATH DE number 4039251 (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 1841809 (Why is no real title available?)
- scientific article; zbMATH DE number 1878545 (Why is no real title available?)
- scientific article; zbMATH DE number 2090840 (Why is no real title available?)
- scientific article; zbMATH DE number 3351184 (Why is no real title available?)
- scientific article; zbMATH DE number 2242579 (Why is no real title available?)
- A calculus and logic of resources and processes
- A hard act to follow
- An axiomatic proof technique for parallel programs
- Anytime, anywhere: modal logics for mobile ambients
- CONCUR 2004 - Concurrency Theory
- Concurrent manipulation of binary search trees
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- Foundations of Software Science and Computation Structures
- Linear logic
- Monitors
- Permission accounting in separation logic
- Proofs of Networks of Processes
- Representation independence, confinement and access control (extended abstract)
- Separation and information hiding
- The Logic of Bunched Implications
- The nucleus of a multiprogramming system
- The temporal semantics of concurrent programs
- Towards imperative modules: reasoning about invariants and sharing of mutable state
- Variables as resource in separation logic
- Verifying properties of parallel programs
Cited in
(88)- Reasoning about separation using abstraction and reification
- Inter-process buffers in separation logic with rely-guarantee
- Separation Logic Semantics for Communicating Processes
- A relational shape abstract domain
- Explanation of two non-blocking shared-variable communication algorithms
- Programming Languages and Systems
- Barriers in Concurrent Separation Logic
- Verified software toolchain (invited talk)
- A logic of separating modalities
- Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example
- Unary-determined distributive \(\ell \)-magmas and bunched implication algebras
- A program construction and verification tool for separation logic
- Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper)
- Product programs in the wild: retrofitting program verifiers to check information flow security
- Algebra and logic for access control
- Iris from the ground up: a modular foundation for higher-order concurrent separation logic
- Possible values: exploring a concept for concurrency
- Transitive Separation Logic
- Elucidating concurrent algorithms via layers of abstraction and reification
- Fine-grained concurrency with separation logic
- Abstract local reasoning for concurrent libraries: mind the gap
- Reasoning about block-based cloud storage systems via separation logic
- A formally verified compiler back-end
- Precision and the conjunction rule in concurrent separation logic
- Verification of concurrent systems with VerCors
- Algebra and logic for resource-based systems modelling
- A process calculus BigrTiMo of mobile systems and its formal semantics
- A calculus and logic of bunched resources and processes
- Behaviour approximated on subgroups
- A semantics for concurrent separation logic
- On the relation between concurrent separation logic and concurrent Kleene algebra
- The essence of higher-order concurrent separation logic
- Fifty years of Hoare's logic
- Decision problems in a logic for reasoning about reconfigurable distributed systems
- Balancing expressiveness in formal approaches to concurrency
- A verifiable low-level concurrent programming model based on colored Petri nets
- Formal verification of concurrent programs with Read-write locks
- A perspective on specifying and verifying concurrent modules
- A UTP approach for rTiMo
- scientific article; zbMATH DE number 1479626 (Why is no real title available?)
- Complexity optimal decision procedure for a propositional dynamic logic with parallel composition
- Temporary read-only permissions for separation logic
- Blaming the client: on data refinement in the presence of pointers
- An adaptation-complete proof system for local reasoning about cloud storage systems
- A higher-order logic for concurrent termination-preserving refinement
- Spatial-behavioral types for concurrency and resource control in distributed systems
- Syntactic soundness proof of a type-and-capability system with hidden state
- Caper
- Higher-order separation logic in Isabelle/HOLCF
- Concurrent Kleene Algebra
- A game semantics of concurrent separation logic
- Synchronizing the asynchronous
- Verification of component-based systems with recursive architectures
- Algebraic separation logic
- Concurrent Kleene algebra and its foundations
- Graphical models of separation logic
- Fairness, resources, and separation
- Improving thread-modular abstract interpretation
- Concurrent separation logic and operational semantics
- Stone-type dualities for separation logics
- Unified reasoning about robustness properties of symbolic-heap separation logic
- Strong-separation logic
- Automated verification of parallel nested DFS
- A substructural epistemic resource logic
- Extracting total Amb programs from proofs
- Steps in modular specifications for concurrent modules (invited tutorial paper)
- Local Data Race Freedom with Non-multi-copy Atomicity
- Connecting higher-order separation logic to a first-order outside world
- A predicate transformer for choreographies. Computing preconditions in choreographic programming
- Multimodal Separation Logic for Reasoning About Operational Semantics
- Syntactic regions for concurrent programs
- A resource analysis of the \(\pi\)-calculus
- Granularity and concurrent separation logic
- An algebraic glimpse at bunched implications and separation logic
- Automatic Parallelization and Optimization of Programs by Proof Rewriting
- RHLE: modular deductive verification of relational \(\forall \exists\) properties
- A step-indexed Kripke model of hidden state
- Separation Logic Tutorial
- Syntactic control of interference and concurrent separation logic
- Abstract specifications for concurrent maps
- Specifying and reasoning about shared-variable concurrency
- Practical abstractions for automated verification of message passing concurrency
- Revisiting concurrent separation logic
- Weakening Relation Algebras and FL$$^2$$-algebras
- Abstract hidden Markov models: a monadic account of quantitative information flow
- Aneris: a mechanised logic for modular reasoning about distributed systems
- Separation Logic Contracts for a Java-Like Language with Fork/Join
- Certificates and Separation Logic
This page was built for publication: Resources, concurrency, and local reasoning
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q879368)
