### Abstract

These components formalise a semantic framework for the deductive verification of hybrid systems. They support reasoning about continuous evolutions of hybrid programs in the style of differential dynamics logic. Vector fields or flows model these evolutions, and their verification is done with invariants for the former or orbits for the latter. Laws of modal Kleene algebra or categorical predicate transformers implement the verification condition generation. Examples show the approach at work.

### License

BSD License

### History

December 13, 2020
  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.

### Topics

- Mathematics/Algebra
- Mathematics/Analysis

### Session Hybrid_Systems_VCs

- HS_Preliminaries
- HS_ODEs
- HS_VC_Spartan
- HS_VC_Examples
- HS_VC_PT
- HS_VC_PT_Examples
- HS_VC_MKA
- HS_VC_KA_rel
- HS_VC_MKA_rel
- HS_VC_MKA_Examples_rel
- HS_VC_KA_ndfun
- HS_VC_MKA_ndfun
- HS_VC_MKA_Examples_ndfun
- HS_VC_KAT
- HS_VC_KAT_rel
- HS_VC_KAT_Examples_rel
- HS_VC_KAT_ndfun
- HS_VC_KAT_Examples_ndfun

### Depends on

- Kleene Algebras with Domain
- Kleene Algebra with Tests and Demonic Refinement Algebras
- Ordinary Differential Equations
- Transformer Semantics

### Used by

- Matrices for ODEs

### Auto-related entries

- A Separation Logic Framework for Imperative HOL
- Refinement for Monadic Programs

## Cite

×

Hybrid_Systems_VCs-AFP

    @article{Hybrid_Systems_VCs-AFP,
      author  = {Jonathan Julian Huerta y Munive},
      title   = {Verification Components for Hybrid Systems},
      journal = {Archive of Formal Proofs},
      month   = {September},
      year    = {2019},
      note    = {\url{https://isa-afp.org/entries/Hybrid_Systems_VCs.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Sep 10, 2019 : Isabelle2019