Added components based on Kleene algebras with tests. These implement differential Hoare logic (dH) and a Morgan-style differential refinement calculus (dR) for verification of hybrid programs. Generalised theorems about invariants of systems of ODEs.
Description
Description
Details
Details
- Provenance
Jonathan Julian Huerta y Munive <jonjulian23@gmail.com> Authored on - Parents
- rAFP1cc03815b90c: replaced concrete nat and bool by abstract types
- Branches
- Unknown
- Tags