Iris from the ground up: A modular foundation for higher-order concurrent separation logic
From MaRDI portal
Publication:4625160
DOI10.1017/S0956796818000151zbMath1476.68062OpenAlexW2901454403WikidataQ128902034 ScholiaQ128902034MaRDI QIDQ4625160
Derek R. Dreyer, Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal
Publication date: 20 February 2019
Published in: Journal of Functional Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s0956796818000151
Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Formalization of mathematics in connection with theorem provers (68V20)
Related Items
Verifying Visibility-Based Weak Consistency, Local Reasoning for Global Graph Properties, Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems, RustHorn: CHC-Based Verification for Rust Programs, Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper), Ghost signals: verifying termination of busy waiting, Abstraction and subsumption in modular verification of C programs, Generalized arrays for Stainless frames, Reasoning about iteration and recursion uniformly based on big-step semantics, Certified verification of relational properties, Operationally-based program equivalence proofs using LCTRSs, When programs have to watch paint dry, Concise outlines for a complex logic: a proof outline checker for TaDA, Foundations for entailment checking in quantitative separation logic, Extracting total Amb programs from proofs, Unnamed Item, Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library, Local local reasoning: a BI-hyperdoctrine for full ground store, Effect algebras, Girard quantales and complementation in separation logic, Unnamed Item, Iris from the ground up: A modular foundation for higher-order concurrent separation logic, Verified software units, Temporal refinements for guarded recursive types, Unnamed Item, Unnamed Item, Unnamed Item, Linear capabilities for fully abstract compilation of separation-logic-verified code, StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities, A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The category-theoretic solution of recursive metric-space equations
- Solving reflexive domain equations in a category of complete metric spaces
- A semantics for concurrent separation logic
- Resources, concurrency, and local reasoning
- Proving assertions about parallel programs
- A perspective on specifying and verifying concurrent modules
- Verified tail bounds for randomized programs
- On models of higher-order separation logic
- Monads on symmetric monoidal closed categories
- Strong functors and monoidal monads
- Viper: A Verification Infrastructure for Permission-Based Reasoning
- Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity
- Iris
- Fictional Separation Logic
- Views
- Subjective auxiliary state for coarse-grained concurrency
- Higher-order ghost state
- The Essence of Higher-Order Concurrent Separation Logic
- A Higher-Order Logic for Concurrent Termination-Preserving Refinement
- Dafny: An Automatic Program Verifier for Functional Correctness
- First steps in synthetic guarded domain theory: step-indexing in the topos of trees
- Packaging Mathematical Structures
- A very modal model of a modern, major, general type system
- Local Reasoning for Storable Locks and Threads
- A Marriage of Rely/Guarantee and Separation Logic
- Reasoning about Optimistic Concurrency Using a Program Logic for History
- Deny-Guarantee Reasoning
- Guarded commands, nondeterminacy and formal derivation of programs
- The Logic of Bunched Implications
- Iris from the ground up: A modular foundation for higher-order concurrent separation logic
- Syntactic soundness proof of a type-and-capability system with hidden state
- Bringing Order to the Separation Logic Jungle
- ReLoC
- Superficially substructural types
- BI as an assertion language for mutable data structures
- Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency
- A theory of indirection via approximation
- A relational modal logic for higher-order stateful ADTs
- Local rely-guarantee reasoning
- Permission accounting in separation logic
- Interactive proofs in higher-order concurrent separation logic
- A relational model of types-and-effects in higher-order concurrent separation logic
- Verified Compilation for Shared-Memory C
- Impredicative Concurrent Abstract Predicates
- Communicating State Transition Systems for Fine-Grained Concurrent Resources
- Multimodal Separation Logic for Reasoning About Operational Semantics
- Oracle Semantics for Concurrent Separation Logic
- Theorem Proving in Higher Order Logics
- Program Logics for Certified Compilers
- Step-Indexed Kripke Model of Separation Logic for Storable Locks
- On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning
