Pages that link to "Item:Q2486585"
From MaRDI portal
The following pages link to Proving pointer programs in higher-order logic (Q2486585):
Displaying 16 items.
- Invariant diagrams with data refinement (Q432148) (← links)
- Certifying assembly with formal security proofs: the case of BBS (Q436406) (← links)
- Formal study of functional orbits in finite domains (Q483296) (← links)
- Inter-process buffers in separation logic with rely-guarantee (Q613139) (← links)
- Reasoning about memory layouts (Q633298) (← links)
- Juggrnaut: using graph grammars for abstracting unbounded heap structures (Q746781) (← links)
- Formal verification of C systems code. Structured types, separation logic and theorem proving (Q835768) (← links)
- Formal verification of a C-like memory model and its uses for verifying program transformations (Q945054) (← links)
- Convergence: integrating termination and abort-freedom (Q1647960) (← links)
- A Program Construction and Verification Tool for Separation Logic (Q2941173) (← links)
- Data Refinement of Invariant Based Programs (Q2994494) (← links)
- Reasoning about Assignments in Recursive Data Structures (Q2999318) (← links)
- Verification of the Schorr-Waite Algorithm – From Trees to Graphs (Q3003486) (← links)
- A Machine-Checked Framework for Relational Separation Logic (Q3095237) (← links)
- Practical Tactics for Separation Logic (Q3183539) (← links)
- Lightweight Separation (Q3543659) (← links)
