Resources, concurrency, and local reasoning

DOI10.1016/j.tcs.2006.12.035zbMath1111.68023OpenAlexW2132761501WikidataQ29544774 ScholiaQ29544774MaRDI QIDQ879368

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

zbMATH Keywords

concurrency separation logic logics of programs

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Logic in computer science (03B70)

Related Items

Local Data Race Freedom with Non-multi-copy Atomicity, Automated Verification of Parallel Nested DFS, Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems, Connecting Higher-Order Separation Logic to a First-Order Outside World, Abstract local reasoning for concurrent libraries: mind the gap, A UTP approach for rTiMo, A game semantics of concurrent 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, A logic of separating modalities, Possible values: exploring a concept for concurrency, Caper, Fairness, Resources, and Separation, Syntactic Control of Interference and Concurrent Separation Logic, Improving thread-modular abstract interpretation, Concurrent Kleene Algebra, Transitive Separation Logic, A perspective on specifying and verifying concurrent modules, A verifiable low-level concurrent programming model based on colored Petri nets, Formal verification of concurrent programs with Read-write locks, Revisiting concurrent separation logic, A formally verified compiler back-end, A semantics for concurrent separation logic, A Program Construction and Verification Tool for Separation Logic, Blaming the client: on data refinement in the presence of pointers, Inter-process buffers in separation logic with rely-guarantee, Weakening Relation Algebras and FL$$^2$$-algebras, Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example, Balancing expressiveness in formal approaches to concurrency, Specifying graph languages with type graphs, Extracting total Amb programs from proofs, A predicate transformer for choreographies. Computing preconditions in choreographic programming, RHLE: modular deductive verification of relational $\forall \exists$ properties, An algebraic glimpse at bunched implications and separation logic, A calculus and logic of bunched resources and processes, Unnamed Item, Unary-determined distributive $\ell $-magmas and bunched implication algebras, Verification of component-based systems with recursive architectures, Steps in modular specifications for concurrent modules (invited tutorial paper), Iris from the ground up: A modular foundation for higher-order concurrent separation logic, Temporary Read-Only Permissions for Separation Logic, Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic, The Essence of Higher-Order Concurrent Separation Logic, A Higher-Order Logic for Concurrent Termination-Preserving Refinement, Abstract Specifications for Concurrent Maps, Explanation of two non-blocking shared-variable communication algorithms, Spatial-behavioral types for concurrency and resource control in distributed systems, Verified Software Toolchain, Barriers in Concurrent Separation Logic, Strong-separation logic, A step-indexed Kripke model of hidden state, Syntactic soundness proof of a type-and-capability system with hidden state, Unnamed Item, Separation Logic Semantics for Communicating Processes, Multimodal Separation Logic for Reasoning About Operational Semantics, Higher-Order Separation Logic in Isabelle/HOLCF, All-Path Reachability Logic, Elucidating concurrent algorithms via layers of abstraction and reification, Algebra and logic for access control, Precision and the Conjunction Rule in Concurrent Separation Logic, A Resource Analysis of the π-calculus, Concurrent Separation Logic and Operational Semantics, Verification of Concurrent Systems with VerCors, Algebraic separation logic, Concurrent Kleene algebra and its foundations, A process calculus BigrTiMo of mobile systems and its formal semantics, Graphical models of separation logic, Fifty years of Hoare's logic, Unnamed Item, Complexity Optimal Decision Procedure for a Propositional Dynamic Logic with Parallel Composition, Granularity and Concurrent Separation Logic, A relational shape abstract domain, A Substructural Epistemic Resource Logic, Automatic Parallelization and Optimization of Programs by Proof Rewriting, Algebra and logic for resource-based systems modelling, Certificates and Separation Logic, Fine-grained concurrency with separation logic, Behaviour approximated on subgroups, An adaptation-complete proof system for local reasoning about cloud storage systems, Reasoning about block-based cloud storage systems via separation logic, Separation Logic Tutorial, Separation Logic Contracts for a Java-Like Language with Fork/Join, Decision problems in a logic for reasoning about reconfigurable distributed systems, On the relation between concurrent separation logic and concurrent Kleene algebra, Reasoning about Separation Using Abstraction and Reification

Uses Software

SLMC

Cites Work