KeYmaera

KeYmaera: A hybrid theorem prover for hybrid systems. KeYmaera is a hybrid verification tool for hybrid systems that combines deductive, real algebraic, and computer algebraic prover technologies. It is an automated and interactive theorem prover for a natural specification and verification logic for hybrid systems. KeYmaera supports differential dynamic logic, which is a real-valued first-order dynamic logic for hybrid programs, a program notation for hybrid automata. For automating the verification process, KeYmaera implements a generalized free-variable sequent calculus and automatic proof strategies that decompose the hybrid system specification symbolically. To overcome the complexity of real arithmetic, we integrate real quantifier elimination following an iterative background closure strategy. Our tool is particularly suitable for verifying parametric hybrid systems and has been used successfully for verifying collision avoidance in case studies from train control and air traffic management.


References in zbMATH (referenced in 40 articles , 1 standard article )

Showing results 1 to 20 of 40.
Sorted by year (citations)

1 2 next

  1. Huang, Yanhong; Pang, Haiping; Shi, Jianqi: Modeling and verification of a timing protection mechanism in the OSEK/VDX OS using CSP (2020)
  2. Suenaga, Kohei; Ishizawa, Takuya: Generalized property-directed reachability for hybrid systems (2020)
  3. Tsachouridis, Vassilios A.; Giantamidis, Georgios; Basagiannis, Stylianos; Kouramas, Kostas: Formal analysis of the Schulz matrix inversion algorithm: a paradigm towards computer aided verification of general matrix flow solvers (2020)
  4. Bohrer, Brandon; Fernández, Manuel; Platzer, André: (\mathsfdL_\iota): definite descriptions in differential dynamic logic (2019)
  5. Huang, Zongyan; England, Matthew; Wilson, David J.; Bridge, James; Davenport, James H.; Paulson, Lawrence C.: Using machine learning to improve cylindrical algebraic decomposition (2019)
  6. Platzer, André: Uniform substitution at one Fell swoop (2019)
  7. Sogokon, Andrew; Jackson, Paul B.; Johnson, Taylor T.: Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants (2019)
  8. Doyen, Laurent; Frehse, Goran; Pappas, George J.; Platzer, André: Verification of hybrid systems (2018)
  9. Platzer, André: Uniform substitution for differential game logic (2018)
  10. Rahli, Vincent; Cohen, Liron; Bickford, Mark: A verified theorem prover backend supported by a monotonic library (2018)
  11. Dreossi, Tommaso: Sapo: reachability computation and parameter synthesis of polynomial dynamical systems (2017)
  12. Dreossi, Tommaso; Dang, Thao; Piazza, Carla: Reachability computation for polynomial dynamical systems (2017)
  13. Fulton, Nathan; Mitsch, Stefan; Bohrer, Brandon; Platzer, André: Bellerophon: tactical theorem proving for hybrid systems (2017)
  14. Müller, Andreas; Mitsch, Stefan; Retschitzegger, Werner; Schwinger, Wieland; Platzer, André: Change and delay contracts for hybrid system component verification (2017)
  15. Platzer, André: A complete uniform substitution calculus for differential dynamic logic (2017)
  16. Avigad, Jeremy; Lewis, Robert Y.; Roux, Cody: A heuristic prover for real inequalities (2016)
  17. Bernardeschi, Cinzia; Domenici, Andrea: Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system (2016)
  18. Konečný, Michal; Taha, Walid; Bartha, Ferenc A.; Duracz, Jan; Duracz, Adam; Ames, Aaron D.: Enclosing the behavior of a hybrid automaton up to and beyond a Zeno point (2016)
  19. Mitsch, Stefan; Platzer, André: ModelPlex: verified runtime validation of verified cyber-physical system models (2016)
  20. Navarro-López, Eva M.; Carter, Rebekah: Deadness and how to disprove liveness in hybrid dynamical systems (2016)

1 2 next