The KeYmaera X Proof IDE - Concepts on Usability in Hybrid Systems Theorem Proving

Stefan Mitsch
(Computer Science Department, Carnegie Mellon University)
André Platzer
(Computer Science Department, Carnegie Mellon University)

Hybrid systems verification is quite important for developing correct controllers for physical systems, but is also challenging. Verification engineers, thus, need to be empowered with ways of guiding hybrid systems verification while receiving as much help from automation as possible. Due to undecidability, verification tools need sufficient means for intervening during the verification and need to allow verification engineers to provide system design insights.

This paper presents the design ideas behind the user interface for the hybrid systems theorem prover KeYmaera X. We discuss how they make it easier to prove hybrid systems as well as help learn how to conduct proofs in the first place. Unsurprisingly, the most difficult user interface challenges come from the desire to integrate automation and human guidance. We also share thoughts how the success of such a user interface design could be evaluated and anecdotal observations about it.

In Catherine Dubois, Paolo Masci and Dominique Méry: Proceedings of the Third Workshop on Formal Integrated Development Environment (F-IDE 2016), Limassol, Cyprus, November 8, 2016, Electronic Proceedings in Theoretical Computer Science 240, pp. 67–81.
Published: 27th January 2017.

ArXived at: http://dx.doi.org/10.4204/EPTCS.240.5 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org