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

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

1 2 next

  1. Dreossi, Tommaso; Dang, Thao; Piazza, Carla: Reachability computation for polynomial dynamical systems (2017)
  2. Avigad, Jeremy; Lewis, Robert Y.; Roux, Cody: A heuristic prover for real inequalities (2016)
  3. Bernardeschi, Cinzia; Domenici, Andrea: Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system (2016)
  4. 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)
  5. Navarro-López, Eva M.; Carter, Rebekah: Deadness and how to disprove liveness in hybrid dynamical systems (2016)
  6. Aréchiga, Nikos; Kapinski, James; Deshmukh, Jyotirmoy V.; Platzer, André; Krogh, Bruce: Numerically-aided deductive safety proof for a powertrain control system (2015)
  7. Fulton, Nathan; Mitsch, Stefan; Quesel, Jan-David; Völp, Marcus; Platzer, André: KeYmaera X: an axiomatic tactical theorem prover for hybrid systems (2015)
  8. Hulette, Geoffrey C.; Armstrong, Robert C.; Mayo, Jackson R.; Ruthruff, Joseph R.: Theorem-proving analysis of digital control logic interacting with continuous dynamics (2015)
  9. Matsumoto, Shota; Kono, Fumihiko; Kobayashi, Teruya; Ueda, Kazunori: HyLaGi: symbolic implementation of a hybrid constraint language HydLa (2015) ioport
  10. Platzer, André: Differential game logic (2015)
  11. Rebiha, Rachid; Moura, Arnaldo V.; Matringe, Nadir: Generating invariants for non-linear hybrid systems (2015)
  12. Mitsch, Stefan; Passmore, Grant Olney; Platzer, André: Collaborative verification-driven engineering of hybrid systems (2014) ioport
  13. Ahrendt, Wolfgang; Dylla, Maximilian: A system for compositional verification of asynchronous objects (2012)
  14. Benvenuti, Luca; Bresolin, Davide; Collins, Pieter; Ferrari, Alberto; Geretti, Luca; Villa, Tiziano: Ariadne: dominance checking of nonlinear hybrid automata using reachability analysis (2012)
  15. Quesel, Jan-David; Platzer, André: Playing hybrid games with KeYmaera (2012)
  16. Höfner, Peter; Möller, Bernhard: Fixing Zeno gaps (2011)
  17. Quesel, Jan-David; Fränzle, Martin; Damm, Werner: Crossing the bridge between similar games (2011)
  18. Suenaga, Kohei; Hasuo, Ichiro: Programming with infinitesimals: a While-language for hybrid system modeling (2011)
  19. Platzer, André: Differential-algebraic dynamic logic for differential-algebraic programs (2010)
  20. Platzer, André; Clarke, Edmund M.: Computing differential invariants of hybrid systems as fixed points (2009)

1 2 next