TY - GEN
T1 - The KeY System 1.0 (Deduction Component)
AU - Beckert, Bernhard
AU - Giese, Martin
AU - Schmitt, P. H.
AU - Klebanov, Vladimir
AU - Rümmer, P.
AU - Hähnle, R.
PY - 2007
Y1 - 2007
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/35148862665
U2 - 10.1007/978-3-540-73595-3_26
DO - 10.1007/978-3-540-73595-3_26
M3 - Conference proceedings
SN - 3540735941
SN - 9783540735946
VL - 4603
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 379
EP - 384
BT - Proceedings of CADE-21, Bremen
A2 - Frank Pfenning, null
PB - Springer
CY - Heidelberg
ER -