Verification of Object-Oriented Software:
The KeY Approach

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

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)

Download all (available) examples (ZIP file)

Download an updated version of the examples for use with KeY 1.4 (ZIP file)