KeYmaera
Subproject |
H3 |
Categories |
Theorem prover for hybrid systems |
Overview |
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. |
A. Platzer. Differential-algebraic dynamic logic for differential-algebraic programs. Journal of Logic and Computation, 20(1), pages 309-352, 2010. A. Platzer and J.-D. Quesel. European Train Control System: A case study in formal verification. In Karin Breitman and Ana Cavalcanti, editors, 11th International Conference on Formal Engineering Methods (ICFEM), volume 5885 of Lecture Notes in Computer Science (LNCS), pages 246-265, 2009. A. Platzer, J.-D. Quesel, and P. Rümmer. Real world verification. In Renate A. Schmidt, editor, In International Conference on Automated Deduction (CADE), volume 5663 of Lecture Notes in Computer Science (LNCS), pages 485-501, 2009. A. Platzer and E.M. Clarke. Computing differential invariants of hybrid systems as fixedpoints. Formal Methods in System Design, 35(1), pages 98-120, 2009. A. Platzer and E.M. Clarke. Formal verification of curved flight collision avoidance maneuvers: A case study. In Ana Cavalcanti and Dennis Dams, editors, 16th International Symposium on Formal Methods (FM), volume 5850 of Lecture Notes in Computer Science (LNCS), pages 547-562, 2009. A. Platzer. Differential dynamic logic for hybrid systems. Journal of Automated Reasoning, 41(2), pages 143-189, 2008. A. Platzer and J.-D. Quesel. KeYmaera: A hybrid theorem prover for hybrid systems. In Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors, 3rd International Joint Conference on Automated Reasoning (IJCAR), volume 5195 of Lecture Notes in Computer Science (LNCS), pages 171-178, 2008. |
|
ETCS Example, RCAS Example |
|
Download |
|
Manual |
|
Status |
Stable |