@inproceedings{394cf3b682cf439f9a66d5be137673b4,
title = "The KeY System 1.0 (Deduction Component)",
abstract = "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.",
author = "Bernhard Beckert and Martin Giese and Schmitt, {P. H.} and Vladimir Klebanov and P. R{\"u}mmer and R. H{\"a}hnle",
year = "2007",
language = "English",
isbn = "978-3-540-73594-6",
volume = "4603",
series = "Lecture Notes in Computer Science (LNCS)",
publisher = "Springer",
pages = "379--384",
editor = "{Frank Pfenning}",
booktitle = "Proceedings of CADE-21, Bremen",
}