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. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Beckert, B., Giese, M., Hähnle, R., Klebanov, V., Rümmer, P., Schlager, S., & Schmitt, P. H. (2007). The KeY system 1.0 (deduction component). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4603 LNAI, pp. 379–384). Springer Verlag. https://doi.org/10.1007/978-3-540-73595-3_26
Mendeley helps you to discover research relevant for your work.