The KeY System 1.0 (Deduction Component)
Bernhard Beckert, Martin Giese, Reiner H\"ahnle, Vladimir Klebanov,
Philipp R\"ummer, Steffen Schlager, and Peter H. Schmitt
The KeY system is a development of the ongoing KeY project, whose aim
is to integrate formal specification and deductive verification into
the industrial software engineering processes. The deductive component
of the KeY system is a novel interactive/automated prover for
first-order Dynamic Logic for Java. The KeY prover features a
user-friendly graphical interface, a backtracking-free free-variable
sequent calculus with equality, a simple and powerful theory
formalization language called "taclets," solution procedures for
linear and non-linear integer arithmetic, external theorem prover
integration, and facilities for proof reuse, among other aspects. The
system is publicly available.