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.
Keywords for this software
References in zbMATH (referenced in 17 articles , 1 standard article )
Showing results 1 to 17 of 17.
Sorted by year (- Avigad, Jeremy; Lewis, Robert Y.; Roux, Cody: A heuristic prover for real inequalities (2016)
- Bernardeschi, Cinzia; Domenici, Andrea: Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system (2016)
- 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)
- Navarro-López, Eva M.; Carter, Rebekah: Deadness and how to disprove liveness in hybrid dynamical systems (2016)
- Aréchiga, Nikos; Kapinski, James; Deshmukh, Jyotirmoy V.; Platzer, André; Krogh, Bruce: Numerically-aided deductive safety proof for a powertrain control system (2015)
- Fulton, Nathan; Mitsch, Stefan; Quesel, Jan-David; Völp, Marcus; Platzer, André: KeYmaera X: an axiomatic tactical theorem prover for hybrid systems (2015)
- Hulette, Geoffrey C.; Armstrong, Robert C.; Mayo, Jackson R.; Ruthruff, Joseph R.: Theorem-proving analysis of digital control logic interacting with continuous dynamics (2015)
- Matsumoto, Shota; Kono, Fumihiko; Kobayashi, Teruya; Ueda, Kazunori: HyLaGi: symbolic implementation of a hybrid constraint language HydLa (2015)
- Rebiha, Rachid; Moura, Arnaldo V.; Matringe, Nadir: Generating invariants for non-linear hybrid systems (2015)
- Mitsch, Stefan; Passmore, Grant Olney; Platzer, André: Collaborative verification-driven engineering of hybrid systems (2014)
- Ahrendt, Wolfgang; Dylla, Maximilian: A system for compositional verification of asynchronous objects (2012)
- Quesel, Jan-David; Platzer, André: Playing hybrid games with keymaera (2012)
- Höfner, Peter; Möller, Bernhard: Fixing Zeno gaps (2011)
- Platzer, André: Differential-algebraic dynamic logic for differential-algebraic programs (2010)
- Platzer, André; Clarke, Edmund M.: Computing differential invariants of hybrid systems as fixed points (2009)
- Platzer, André; Clarke, Edmund M.: Computing differential invariants of hybrid systems as fixedpoints (2008)
- Platzer, André; Quesel, Jan-David: KeYmaera: A hybrid theorem prover for hybrid systems. (System description) (2008)