RISC RISC Research Institute for Symbolic Computation  
  • @inproceedings{RISC3373,
    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}