The following pages link to (Q4783297):
Displaying 22 items.
- A logic of separating modalities (Q290917) (← links)
- A verifiable low-level concurrent programming model based on colored Petri nets (Q350966) (← links)
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic (Q436400) (← links)
- Verification conditions for source-level imperative programs (Q465685) (← links)
- The dynamic frames theory (Q539422) (← links)
- Algebraic separation logic (Q549676) (← links)
- Inter-process buffers in separation logic with rely-guarantee (Q613139) (← links)
- Trace-based verification of imperative programs with I/O (Q617977) (← links)
- Frame rule for mutually recursive procedures manipulating pointers (Q732009) (← links)
- Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper) (Q832157) (← links)
- Ghost signals: verifying termination of busy waiting (Q832247) (← links)
- Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms (Q832310) (← links)
- Formal verification of C systems code. Structured types, separation logic and theorem proving (Q835768) (← links)
- On Temporal and Separation Logics (Q5079764) (← links)
- (Q5111651) (← links)
- Propositional Dynamic Logic with Storing, Recovering and Parallel Composition (Q5179014) (← links)
- Separation Logic Semantics for Communicating Processes (Q5415605) (← links)
- Multimodal Separation Logic for Reasoning About Operational Semantics (Q5415628) (← links)
- Higher-Order Separation Logic in Isabelle/HOLCF (Q5415649) (← links)
- A Resource Analysis of the π-calculus (Q5739364) (← links)
- A proof procedure for separation logic with inductive definitions and data (Q6053843) (← links)
- Concise outlines for a complex logic: a proof outline checker for TaDA (Q6145023) (← links)
