Pages that link to "Item:Q1977126"
From MaRDI portal
The following pages link to Hoare logic and auxiliary variables (Q1977126):
Displaying 19 items.
- Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control (Q444460) (← links)
- Verification conditions for source-level imperative programs (Q465685) (← links)
- The spirit of ghost code (Q518394) (← links)
- Structural operational semantics through context-dependent behaviour (Q638568) (← links)
- Toward automatic verification of quantum programs (Q667515) (← links)
- Building program construction and verification tools from algebraic principles (Q736461) (← links)
- Balancing the load. Leveraging a semantics stack for systems verification (Q835780) (← links)
- Model-based specification (Q1607085) (← links)
- Calculating sharp adaptation rules. (Q1607103) (← links)
- An adaptation-complete proof system for local reasoning about cloud storage systems (Q2072067) (← links)
- Abstraction and subsumption in modular verification of C programs (Q2147702) (← links)
- Verified software units (Q2233451) (← links)
- Fifty years of Hoare's logic (Q2280214) (← links)
- A program logic for resources (Q2463560) (← links)
- Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach (Q2802468) (← links)
- Completeness of Hoare Logic Relative to the Standard Model (Q2971129) (← links)
- Reverse Hoare Logic (Q3095238) (← links)
- Reasoning About Resources in the Embedded Systems Language Hume (Q3460507) (← links)
- Abstraction and subsumption in modular verification of C programs (Q6535970) (← links)
