Local reasoning about programs that alter data structures
From MaRDI portal
Recommendations
Cited in
(only showing first 100 items - show all)- Semantics and logic of object calculi
- Convergence: integrating termination and abort-freedom
- Formally verifying exceptions for low-level code with separation logic
- A formal C memory model for separation logic
- Weak updates and separation logic
- Unifying separation logic and region logic to allow interoperability
- Program logic and equivalence in the presence of garbage collection.
- Model checking mobile ambients
- Correctness of data representations involving heap data structures
- An adaptation-complete proof system for local reasoning about cloud storage systems
- Reasoning about block-based cloud storage systems via separation logic
- Verifying Whiley programs with Boogie
- Category-theoretic structure for independence and conditional independence
- Generalized arrays for Stainless frames
- Separation logic and logics with team semantics
- Parameterized synthesis for fragments of first-order logic over data words
- Local local reasoning: a BI-hyperdoctrine for full ground store
- Decomposing data structure commutativity proofs with \(mn\)-differencing
- Fifty years of Hoare's logic
- Logical vs. behavioural specifications
- Automatically proving termination and memory safety for programs with pointer arithmetic
- Revisiting concurrent separation logic
- Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems
- Temporal property verification as a program analysis task
- Verification of finite iterations over collections of variable data structures
- Effect algebras, Girard quantales and complementation in separation logic
- Proving pointer programs in Hoare logic
- A complete decision procedure for linearly compositional separation logic with data constraints
- Local reasoning about tree update
- Local reasoning about data update
- Manipulating trees with hidden labels
- The laws of programming unify process calculi
- A logic of separating modalities
- Laws of programming for references
- A program construction and verification tool for separation logic
- Unified reasoning about robustness properties of symbolic-heap separation logic
- Reasoning about assignments in recursive data structures
- The relationship between separation logic and implicit dynamic frames
- Verification of the Schorr-Waite algorithm -- from trees to graphs
- Partiality, state and dependent types
- Verifying object-oriented programs with higher-order separation logic in Coq
- A machine-checked framework for relational separation logic
- Completeness for a first-order abstract separation logic
- A Formalisation of Smallfoot in HOL
- Automatic Parallelization and Optimization of Programs by Proof Rewriting
- Bottom-Up Shape Analysis
- Automated theorem proving for assertions in separation logic with all connectives
- A verifiable low-level concurrent programming model based on colored Petri nets
- Safe Modification of Pointer Programs in Refinement Calculus
- Lightweight Separation
- Footprints in Local Reasoning
- Separation Logic
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- Iris from the ground up: a modular foundation for higher-order concurrent separation logic
- Verification conditions for source-level imperative programs
- scientific article; zbMATH DE number 2087445 (Why is no real title available?)
- Protocol combinators for modeling, testing, and execution of distributed systems
- Concise read-only specifications for better synthesis of programs with pointers
- Local reasoning for global graph properties
- A first-order logic with frames
- On temporal and separation logics
- Convolution and concurrency
- Tractability of separation logic with inductive definitions: beyond lists
- scientific article; zbMATH DE number 7407781 (Why is no real title available?)
- Highly automated formal proofs over memory usage of assembly code
- BI as an assertion language for mutable data structures
- Propositional dynamic logic with storing, recovering and parallel composition
- The dynamic frames theory
- Local reasoning for global invariants. I: Region logic
- Decidable logics combining heap structures and data
- Separation Logic Semantics for Communicating Processes
- Multimodal Separation Logic for Reasoning About Operational Semantics
- Higher-order separation logic in Isabelle/HOLCF
- Symbolic Verification Method for Definite Iterations over Tuples of Altered Data Structures and Its Application to Pointer Programs
- Footprints in Local Reasoning
- Algebraic separation logic
- Separation Logic Tutorial
- A Theory of Pointers for the UTP
- Computer Aided Verification
- A resource analysis of the \(\pi\)-calculus
- Program Verification with Separation Logic
- On Composing Finite Forests with Modal Logics
- Typing copyless message passing
- A proof procedure for separation logic with inductive definitions and data
- Inter-process buffers in separation logic with rely-guarantee
- Concise outlines for a complex logic: a proof outline checker for TaDA
- Trace-based verification of imperative programs with I/O
- An algebraic glimpse at bunched implications and separation logic
- Asynchronous Cooperative Contracts for Cooperative Scheduling
- Make flows small again: revisiting the flow framework
- Describing and animating quantum protocols
- Dynamic separation logic
- From program logics towards language logics
- Pomsets with boxes: protection, separation, and locality in concurrent Kleene algebra
- Modular verification of intrusive list and tree data structures in separation logic
- Idempotent resources in separation logic. The heart of \texttt{core} in Iris
- A logical approach to type soundness
- Day algebras
- Equivalence and conditional independence in atomic sheaf logic
- Safety, relative tightness and the probabilistic frame rule
This page was built for publication: Local reasoning about programs that alter data structures
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4783297)
