KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)

By André Platzer, Jan-David Quesel. International Joint Conference on Automated Reasoning, 2008

355 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Software

View Paper: https://www.semanticscholar.org/paper/3ee6a04237e5a1f1b23ac9fba277206a94673803

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

1. Yanni Kouskoulas
2. Jean-Baptiste Jeannin
3. Erik Zawadzki
4. Aurora C. Schmidt
5. Khalil Ghorbal
6. Ryan Gardner
7. André Platzer
8. Rajeev Alur

In Computational Theory and Mathematics

1. Yanni Kouskoulas
2. Jean-Baptiste Jeannin
3. Erik Zawadzki
4. Aurora C. Schmidt
5. Khalil Ghorbal
6. Ryan Gardner
7. André Platzer
8. Rajeev Alur

In Software

1. André Platzer

Citations in the corpus

• A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System (2015, methodology): “The following proposition, proved in KeYmaera, combines both dynamics and shows that the absence of an NMAC of radius rp in (O,~i,~j) is equivalent to the absence of an NMAC of radius sp in (O′,~i′,~j′).”