FM 2016 Tutorial on new KeYmaera X Prover for Hybrid Systems

Dear colleagues,

First of all, it is a distinct pleasure to introduce a stable version of the shiny new KeYmaera X theorem prover for hybrid systems.

http://keymaeraX.org/

If you're around beautiful Cyprus in November, please also come to the KeYmaera X tutorial at FM 2016

http://keymaerax.org/tutorial/FM-2016.html

We will be demonstrating how to conduct hybrid systems verification with KeYmaera X as well as a reasonable subset of its new features.

Early bird registration is til October 6.

As many of you will know already, we have been very busy developing a successor of KeYmaera 3, which is called KeYmaera X.

The successor KeYmaera X is a complete clean-slate implementation of a theorem prover for hybrid systems, featuring a minimal core of just 1700 lines of code that isolates all soundness-critical reasoning.

In addition to providing numerous improvements like a simpler user interface, tactical proof programming, and advanced automation that many users have always dreamed of, the new KeYmaera X provides *almost* all functionality that its predecessor KeYmaera provides.

You may also like that KeYmaera X visually retains the sequent proofs, and provides a web-based user interface that even records tactics for you. KeYmaera X can also run out of the box without the need to install additional tools. Mathematica is still useful but no longer crucial.

If you have any feedback on the new KeYmaera X, please let us know.

Andre