The following pages link to (Q2721096):
Displayed 21 items.
- Verification conditions for source-level imperative programs (Q465685) (← links)
- Formal study of functional orbits in finite domains (Q483296) (← links)
- Blaming the client: on data refinement in the presence of pointers (Q607403) (← links)
- Inter-process buffers in separation logic with rely-guarantee (Q613139) (← links)
- Doomed program points (Q633286) (← links)
- Reasoning about memory layouts (Q633298) (← 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)
- Operating system verification---an overview (Q1040002) (← links)
- The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML (Q1881670) (← links)
- On building cyclic and shared structures in Haskell (Q1941875) (← links)
- A program logic for resources (Q2463560) (← links)
- Verification of finite iterations over collections of variable data structures (Q2467973) (← links)
- Proving pointer programs in higher-order logic (Q2486585) (← links)
- Laws of Programming for References (Q2937790) (← 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)
- Lightweight Separation (Q3543659) (← links)
- Heaps and Data Structures: A Challenge for Automated Provers (Q5200023) (← links)
- Symbolic Verification Method for Definite Iterations over Tuples of Altered Data Structures and Its Application to Pointer Programs (Q5452196) (← links)