Pages that link to "Item:Q5176992"
From MaRDI portal
The following pages link to Characteristic formulae for the verification of imperative programs (Q5176992):
Displaying 22 items.
- A formalization of programs in first-order logic with a discrete linear order (Q274400) (← links)
- Symbolic execution proofs for higher order store programs (Q287265) (← links)
- An observationally complete program logic for imperative higher-order functions (Q387994) (← links)
- Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits (Q670699) (← links)
- Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms (Q832310) (← links)
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL (Q1722647) (← links)
- Refinement to imperative HOL (Q1739909) (← links)
- A framework for the verification of certifying computations (Q2351144) (← links)
- Implementing and reasoning about hash-consed data structures in Coq (Q2351422) (← links)
- From Sets to Bits in Coq (Q2798253) (← links)
- Formalizing the Edmonds-Karp Algorithm (Q2829260) (← links)
- Refinement to Imperative/HOL (Q2945637) (← links)
- Temporary Read-Only Permissions for Separation Logic (Q2988642) (← links)
- Verified Characteristic Formulae for CakeML (Q2988660) (← links)
- Cogent: uniqueness types and certifying compilation (Q5019022) (← links)
- Trustworthy Graph Algorithms (Invited Talk) (Q5092359) (← links)
- (Q5875421) (← links)
- (Q5875426) (← links)
- (Q5875428) (← links)
- (Q5875432) (← links)
- Characteristic formulae for liveness properties of non-terminating CakeML programs (Q5875446) (← links)
- (Q6060675) (← links)
