Affine systems of ODEs in Isabelle/HOL for hybrid-program verification

DOI10.1007/978-3-030-58768-0_5zbMath1476.68301OpenAlexW3085046366MaRDI QIDQ2038037

Jonathan Julián Huerta y Munive

Publication date: 8 July 2021

Full work available at URL: https://doi.org/10.1007/978-3-030-58768-0_5

zbMATH Keywords

hybrid systemsformal verificationproof assistants

Mathematics Subject Classification ID

Linear ordinary differential equations and systems (34A30) Specification and verification (program logics, model checking, etc.) (68Q60) Formalization of mathematics in connection with theorem provers (68V20)

Related Items (2)

Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL ⋮ \textsf{HHLPy}: practical verification of hybrid systems using Hoare logic

Uses Software

• Isabelle
• Isabelle/HOL
• HOL

This page was built for publication: Affine systems of ODEs in Isabelle/HOL for hybrid-program verification