IsaVODEs: Interactive verification of cyber-physical systems at scale

DOI10.1007/S10817-024-09709-2MaRDI QIDQ6653093zbMATH OpenFDO

Authors Jonathan Julián Huerta y Munive, Simon Foster, Mario Gleirscher, Georg Struth, Christian Pardillo Laursen, Thomas Hickman

Publication date 16 December 2024

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Copyright license Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International

Full work available at URL https://doi.org/10.1007/S10817-024-09709-2

zbMATH Keywords

cyber-physical systemshybrid systemsinteractive theorem provinglensespredicate transformersprogram correctness and verification

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• \textsf{HHLPy}: practical verification of hybrid systems using Hoare logic
• A consistent foundation for Isabelle/HOL
• Affine systems of ODEs in Isabelle/HOL for hybrid-program verification
• Automated Algebraic Reasoning for Collections and Local Variables with Lenses
• Building program construction and verification tools from algebraic principles
• Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL
• Differential equation axiomatization. The impressive power of differential ghosts
• Differential game logic
• Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
• Eisbach: a proof method language for Isabelle
• Hammering towards QED
• scientific article; zbMATH DE number 1556014 (Why is no real title available?)
• Implicit definitions with differential equations for KeYmaera X (system description)
• Integration of formal proof into unified assurance cases with Isabelle/SACM
• JuliaReach
• KeYmaera X: an axiomatic tactical theorem prover for hybrid systems
• Logical analysis of hybrid systems. Proving theorems for complex dynamics.
• Logical foundations of cyber-physical systems
• Logics of dynamical systems
• MetiTarski: An automatic theorem prover for real-valued special functions
• Modal Kleene algebra applied to program correctness
• Ordinary differential equations and dynamical systems
• Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL
• Random coefficient differential equation models for bacterial growth
• Refinement Calculus
• Refinement to imperative HOL
• ROSCoq: robots powered by constructive reals
• The flow of ODEs: formalization of variational equation and Poincaré map
• Type classes and filters for mathematical analysis in Isabelle/HOL
• Verified Quadratic Virtual Substitution for Real Arithmetic

Cited in

(1)

• Shallow Expressions

Describes a project that uses

Uses Software

• SageMath

This page was built for publication: IsaVODEs: Interactive verification of cyber-physical systems at scale

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6653093)