The new book covers deductive software verification as realised by the KeY approach. It constitutes the ultimate source for the KeY tool since version 2.x.
It also features a general (not KeY specific) chapter on the Java Modeling Language which provides a thorough introduction into the specification language.
The book differs significantly from its first edition. Almost all chapters are either new or largely rewritten. It encompasses the experiences learned between the years 2006-2016.
The KeY book is available at Springer Online (LNCS 10001) and at Springer Link.
Table of Contents
1. Quo Vadis Formal Verification?
Part I – Foundations
2. First-Order Logic
3. Dynamic Logic for Java
4. Proof Search with Taclets
5. Theories
6. Abstract Interpretation
Part II – Specification and Verification
7. Formal Specification with the Java Modeling Language
8. From Specification to Proof Obligations
9. Modular Specification and Verification
10. Verifying Java Card Programs
Part III – From Verification to Analysis
11. Debugging and Visualization
12. Proof-based Test Case Generation
13. Information Flow Analysis
14. Program Transformation and Compilation
Part IV – The KeY System in Action
15. Using the KeY Prover
16. Formal Verification with KeY: A Tutorial
17. KeY-Hoare
Part V – Case Studies
18. Verification of an Electronic Voting System
19 Verification of Counting Sort and Radix Sort
Part VI – Appendices
A Java Modeling Language Reference
B KeY File Reference
Errata (found after publishing)
page 30, Figure 2.2
The correct version of the rule eqRight should read:
page 202, Example 7.6
The sentence says
“To specify that a method returns the index of an integer array arr
holding the maximum entry, we can write the following postcondition,” but should say “… the maximum element of an integer array arr.”
page 321, Section 9.3.1 right before Listing 9.8
The last occurrence of accessible before Listing 9.8 must read assignable.
KeY version from the book
The KeY Book describes KeY as in version KeY 2.6.1. Download and additional instructions are available here.
Examples from the book
Annotated Java programs and KeY problem files used in the book may be downloaded here.
Technical report on first-order logic
On page 157 of the KeY book the reader is referred to a technical report on first-order logic for further details. This report may be downloaded here.