The following pages link to Refinement to Imperative/HOL (Q2945637):
Displaying 19 items.
- Formal verification of an executable LTL model checker with partial order reduction (Q682350) (← links)
- A verified SAT solver framework with learn, forget, restart, and incrementality (Q1663234) (← links)
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL (Q1722647) (← links)
- Proof-producing synthesis of CakeML from monadic HOL functions (Q2208292) (← links)
- For a few dollars more. Verified fine-grained algorithm analysis down to LLVM (Q2233462) (← links)
- Automatic refinement to efficient data structures: a comparison of two approaches (Q2417948) (← links)
- Rule-based static analysis of network protocol implementations (Q2482438) (← links)
- Formalizing the Edmonds-Karp Algorithm (Q2829260) (← links)
- Verified Characteristic Formulae for CakeML (Q2988660) (← links)
- Verified Certification of Reachability Checking for Timed Automata (Q5039522) (← links)
- Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs (Q5048997) (← links)
- Efficient Verified Implementation of Introsort and Pdqsort (Q5049010) (← links)
- (Q5875426) (← links)
- (Q5875428) (← links)
- (Q5875431) (← links)
- Efficient verified (UN)SAT certificate checking (Q5919480) (← links)
- Gale-Shapley verified (Q6611960) (← links)
- Refinement of parallel algorithms down to LLVM: applied to practically efficient parallel sorting (Q6611962) (← links)
- Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Pastèque and Nuss-Checker (Q6661748) (← links)
