\textsf{HHLPy}: practical verification of hybrid systems using Hoare logic
From MaRDI portal
Publication:6174532
DOI10.1007/978-3-031-27481-7_11zbMath1529.68164arXiv2210.17163MaRDI QIDQ6174532
Huanhuan Sheng, Alexander Bentkamp, Bohua Zhan
Publication date: 17 August 2023
Published in: Formal Methods (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2210.17163
Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)
Cites Work
- Unnamed Item
- Notions of computation and monads
- Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL
- Differential dynamic logic for hybrid systems
- Verifying hybrid systems with modal Kleene algebra
- Bellerophon: tactical theorem proving for hybrid systems
- A complete uniform substitution calculus for differential dynamic logic
- Affine systems of ODEs in Isabelle/HOL for hybrid-program verification
- A denotational semantics of simulink with higher-order UTP
- Dafny: An Automatic Program Verifier for Functional Correctness
- KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems
- Formal Verification of Simulink/Stateflow Diagrams
- KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)
- Guarded commands, nondeterminacy and formal derivation of programs
- Formal Verification of Simulink/Stateflow Diagrams
- Logical Foundations of Cyber-Physical Systems
- Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
- Differential Equation Invariance Axiomatization
- Why3 — Where Programs Meet Provers
This page was built for publication: \textsf{HHLPy}: practical verification of hybrid systems using Hoare logic
