# Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL

arXiv: https://arxiv.org/abs/1910.13554 · HTML: https://mlsanity.com/paper/1910.13554/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 29 Oct 2019.

## Built on by (most cited first, 2 of 2)

- [Towards Large Language Model Aided Program Refinement](https://mlsanity.com/paper/2406.18616/) (2024)
- [Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving](https://mlsanity.com/paper/2303.09692/) (2023)

## Abstract (arXiv)

We present simple new Hoare logics and refinement calculi for hybrid systems in the style of differential dynamic logic. (Refinement) Kleene algebra with tests is used for reasoning about the program structure and generating verification conditions at this level. Lenses capture hybrid program stores in a generic algebraic way. The approach has been formalised with the Isabelle/HOL proof assistant. A number of examples explains the workflow with the resulting verification components.