Bernhard Beckert, Martin Giese, P. H. Schmitt, Vladimir Klebanov, P. Rümmer, R. Hähnle,
"The KeY System 1.0 (Deduction Component)"
, in Frank Pfenning: Proceedings of CADE-21, Bremen, Serie Lecture Notes in Computer Science (LNCS), Vol. 4603, Springer, Heidelberg, Seite(n) 379-384, 2007, ISBN: 978-3-540-73594-6
Original Titel:
The KeY System 1.0 (Deduction Component)
Sprache des Titels:
Englisch
Original Buchtitel:
Proceedings of CADE-21, Bremen
Original Kurzfassung:
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, 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.