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