KeYmaera swMATH ID: 3709 Software Authors: Platzer, André; Quesel, Jan-David Description: 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. Homepage: http://symbolaris.com/info/KeYmaera.html Keywords: dynamic logic; automated theorem proving; decision procedures; computer algebra; verification of hybrid systems Related Software: SpaceEx; HyTech; KeYmaera X; PHAVer; Isabelle/HOL; Flow*; QEPCAD; z3; MetiTarski; Coq; dReach; RSOLVER; Orbital library; HSolver; Bellerophon; Breach; VeriPhy; ModelPlex; PVS; Differential_Game_Logic Referenced in: 47 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year KeYmaera: A hybrid theorem prover for hybrid systems. (System description). Zbl 1165.68469Platzer, André; Quesel, Jan-David 2008 all top 5 Referenced by 98 Authors 20 Platzer, André 5 Mitsch, Stefan 5 Quesel, Jan-David 2 Bohrer, Brandon 2 Clarke, Edmund Melson jun. 2 Dreossi, Tommaso 2 Fulton, Nathan 2 Paulson, Lawrence Charles 2 Sogokon, Andrew 2 Suenaga, Kohei 2 Tan, Yong Kiam 1 Abhishek, Aakash 1 Ahrendt, Wolfgang 1 Ames, Aaron D. 1 Aréchiga, Nikos 1 Armstrong, Robert C. 1 Avigad, Jeremy 1 Bak, Stanley 1 Bartha, Ferenc Ágoston 1 Basagiannis, Stylianos 1 Benvenuti, Luca 1 Bernardeschi, Cinzia 1 Bickford, Mark 1 Boyer, Benoît 1 Bresolin, Davide 1 Bridge, James P. 1 Carter, Rebekah 1 Cimatti, Alessandro 1 Cohen, Liron 1 Collins, Peter J. 1 Cordwell, Katherine 1 Corso, Anthony 1 Damm, Werner 1 Dang, Thao 1 Davenport, James Harold 1 Deshmukh, Jyotirmoy V. 1 Domenici, Andrea 1 Doyen, Laurent 1 Dragomir, Iulia 1 Duggirala, Parasara Sridhar 1 Duracz, Adam 1 Duracz, Jan 1 Dylla, Maximilian 1 England, Matthew 1 Ferrari, Alberto 1 Fränzle, Martin 1 Frehse, Goran 1 Geretti, Luca 1 Giantamidis, Georgios 1 Griggio, Alberto 1 Hasuo, Ichiro 1 Höfner, Peter 1 Huang, Zongyan 1 Huerta y Munive, Jonathan Julián 1 Hulette, Geoffrey C. 1 Irfan, Ahmed 1 Ishizawa, Takuya 1 Jackson, Paul B. 1 Jeannin, Jean-Baptiste 1 Johnson, Taylor T. 1 Kapinski, James 1 Kastenbaum, Stéphane 1 Kochenderfer, Mykel J. 1 Konečný, Michal 1 Koren, Mark 1 Kouramas, Kostas 1 Krogh, Bruce H. 1 Lee, Ritchie 1 Lewis, Robert Y. 1 Matringe, Nadir 1 Mayo, Jackson R. 1 Möller, Bernhard 1 Moss, Robert J. 1 Moura, Arnaldo Vieira 1 Mover, Sergio 1 Navarro-López, Eva María 1 Pappas, George J. 1 Piazza, Carla 1 Preoteasa, Viorel 1 Rahli, Vincent 1 Rebiha, Rachid 1 Retschitzegger, Werner 1 Roux, Cody 1 Rümmer, Philipp 1 Ruthruff, Joseph R. 1 Sandler, Andrei 1 Schwinger, Wieland 1 Sood, Harry 1 Struth, Georg 1 Taha, Walid 1 Talpin, Jean-Pierre 1 Tonetta, Stefano 1 Tripakis, Stavros 1 Tsachouridis, Vassilios A. 1 Tveretina, Olga 1 Villa, Tiziano 1 Völp, Marcus 1 Wilson, David J. all top 5 Referenced in 13 Serials 4 Journal of Automated Reasoning 4 Formal Methods in System Design 3 Theoretical Computer Science 1 Information Processing Letters 1 Science of Computer Programming 1 Information and Computation 1 Formal Aspects of Computing 1 Journal of Logic and Computation 1 The Journal of Artificial Intelligence Research (JAIR) 1 ACM Transactions on Computational Logic 1 Mathematics in Computer Science 1 Nonlinear Analysis. Hybrid Systems 1 Numerical Algebra, Control and Optimization all top 5 Referenced in 12 Fields 44 Computer science (68-XX) 15 Systems theory; control (93-XX) 11 Mathematical logic and foundations (03-XX) 4 Ordinary differential equations (34-XX) 2 Linear and multilinear algebra; matrix theory (15-XX) 2 Dynamical systems and ergodic theory (37-XX) 2 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 1 Real functions (26-XX) 1 Operator theory (47-XX) 1 Numerical analysis (65-XX) 1 Classical thermodynamics, heat transfer (80-XX) 1 Operations research, mathematical programming (90-XX) Referencing Publications by Year