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 28 articles , 1 standard article )

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

1 2 next

  1. Dreossi, Tommaso: Sapo: reachability computation and parameter synthesis of polynomial dynamical systems (2017)
  2. Dreossi, Tommaso; Dang, Thao; Piazza, Carla: Reachability computation for polynomial dynamical systems (2017)
  3. Fulton, Nathan; Mitsch, Stefan; Bohrer, Brandon; Platzer, André: Bellerophon: tactical theorem proving for hybrid systems (2017)
  4. Platzer, André: A complete uniform substitution calculus for differential dynamic logic (2017)
  5. Avigad, Jeremy; Lewis, Robert Y.; Roux, Cody: A heuristic prover for real inequalities (2016)
  6. Bernardeschi, Cinzia; Domenici, Andrea: Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system (2016)
  7. 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)
  8. Mitsch, Stefan; Platzer, André: ModelPlex: verified runtime validation of verified cyber-physical system models (2016)
  9. Navarro-López, Eva M.; Carter, Rebekah: Deadness and how to disprove liveness in hybrid dynamical systems (2016)
  10. Aréchiga, Nikos; Kapinski, James; Deshmukh, Jyotirmoy V.; Platzer, André; Krogh, Bruce: Numerically-aided deductive safety proof for a powertrain control system (2015)
  11. Fulton, Nathan; Mitsch, Stefan; Quesel, Jan-David; Völp, Marcus; Platzer, André: KeYmaera X: an axiomatic tactical theorem prover for hybrid systems (2015)
  12. Hulette, Geoffrey C.; Armstrong, Robert C.; Mayo, Jackson R.; Ruthruff, Joseph R.: Theorem-proving analysis of digital control logic interacting with continuous dynamics (2015)
  13. Matsumoto, Shota; Kono, Fumihiko; Kobayashi, Teruya; Ueda, Kazunori: HyLaGi: symbolic implementation of a hybrid constraint language HydLa (2015) ioport
  14. Platzer, André: A uniform substitution calculus for differential dynamic logic (2015)
  15. Platzer, André: Differential game logic (2015)
  16. Rebiha, Rachid; Moura, Arnaldo V.; Matringe, Nadir: Generating invariants for non-linear hybrid systems (2015)
  17. Mitsch, Stefan; Passmore, Grant Olney; Platzer, André: Collaborative verification-driven engineering of hybrid systems (2014) ioport
  18. Ahrendt, Wolfgang; Dylla, Maximilian: A system for compositional verification of asynchronous objects (2012)
  19. Benvenuti, Luca; Bresolin, Davide; Collins, Pieter; Ferrari, Alberto; Geretti, Luca; Villa, Tiziano: Ariadne: dominance checking of nonlinear hybrid automata using reachability analysis (2012)
  20. Quesel, Jan-David; Platzer, André: Playing hybrid games with KeYmaera (2012)

1 2 next