Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL

DOI10.1007/s10817-021-09607-xOpenAlexW3210385152MaRDI QIDQ832721

Georg Struth, Jonathan Julián Huerta y Munive

Publication date: 25 March 2022

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

Full work available at URL: https://doi.org/10.1007/s10817-021-09607-x

zbMATH Keywords

hybrid systemspredicate transformersinteractive theorem provinghybrid program verificationmodal Kleene algebra

Mathematics Subject Classification ID

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

Related Items

Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL, \textsf{HHLPy}: practical verification of hybrid systems using Hoare logic, Quantitative Robustness Analysis of Sensor Attacks on Cyber-Physical Systems

Uses Software

• Isabelle/HOL
• KeYmaera
• RODAS
• C-CoRN
• Coquelicot
• Bellerophon
• Archive Formal Proofs
• Ordinary Differential Equations
• Kleene Algebra
• Algebraic_VCs
• KAD
• Differential_Game_Logic
• KeYmaera X
• Transformer semantics
• Quantales

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Internal axioms for domain semirings
• Building program construction and verification tools from algebraic principles
• On the expressive power of Kleene algebra with domain
• Verifying hybrid systems with modal Kleene algebra
• Bellerophon: tactical theorem proving for hybrid systems
• A complete uniform substitution calculus for differential dynamic logic
• The flow of ODEs: formalization of variational equation and Poincaré map
• Coquelicot: a user-friendly library of real analysis for Coq
• Affine systems of ODEs in Isabelle/HOL for hybrid-program verification
• Modal Kleene algebra applied to program correctness
• Generating invariants for non-linear hybrid systems
• Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
• Algebra of Monotonic Boolean Transformers
• Predicate Transformer Semantics
• Verification of Hybrid Systems
• KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems
• Refinement Calculus
• Hoare Semigroups
• Logical Foundations of Cyber-Physical Systems
• The Structure of Differential Invariants and Differential Cut Elimination
• Logical Analysis of Hybrid Systems
• Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
• Differential Equation Axiomatization
• Solving Ordinary Differential Equations II
• Mathematical Knowledge Management
• Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
• The Picard Algorithm for Ordinary Differential Equations in Coq
• Boolean Algebras with Operators. Part I