author = {B. Beckert and M. Giese and R. Hähnle and V. Klebanov and P. Rümmer and S. Schlager and P. H. Schmitt},
title = {{The KeY System 1.0 (Deduction Component)}},
booktitle = {{Proceedings of CADE-21, Bremen}},
language = {english},
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.},
series = {LNCS},
volume = {4603},
pages = {379--384},
publisher = {Springer},
address = {Heidelberg},
isbn_issn = {ISBN 978-3-540-73594-6},
year = {2007},
editor = {Frank Pfenning},
refereed = {yes},
length = {6},
conferencename = {Conference on Automated Deduction}