Bernhard Beckert
Reiner Hähnle
Peter H. Schmitt (Eds.)
Springer-Verlag, LNCS 4334
15 chapters and 2 appendices, xxix + 658 pages
ISBN: 3-540-68977-X
BibTeX Entry | Online Version
The definitive source
for all information related to the KeY project
Table of contents (PDF)
KeY 1.0
KeY 1.0 is the version of the KeY system that is used in the book. It is available for download here (under “older versions”).
Examples from the book
(for use with KeY 1.0)
- Chapter 1: Formal Methods for Software Construction
- Chapter 2: First-Order Logic
- Chapter 3: Dynamic Logic
- Chapter 4: Construction of Proofs
- Chapter 5: Formal Specification
- Chapter 6: Pattern Driven Formal Specification
- Chapter 7: Natural Language Specification
- Chapter 8: Proof Obligations
- Chapter 9: From Sequential Java to Java Card
- Chapter 10: Using KeY
- Chapter 11: Proving by Induction (examples available soon)
- Chapter 12: Java Integers
- Chapter 13: Proof Reuse
- Chapter 14: The Demoney Case Study (unfortunately the case study cannot be published here because the Java source code is copyrighted and not publicly available)
- Chapter 15: The Schorr Waite Algorithm (examples available soon)
Example Updates
- New: Updated examples for KeY 1.6
- Updated examples for KeY 1.4
- Original examples for KeY 1.0