Available at Springer
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.
Preprints are in many cases available on the author’s websites and linked from the table of contents below.
Table of Contents [preprint]
Part I – Foundations
- First-Order Logic [preprint | Springer]
- Dynamic Logic for Java [preprint | Springer]
- Proof Search with Taclets [ preprint | Springer]
- Theories [preprint | Springer]
- Abstract Interpretation [preprint | Springer]
Part II – Specification and Verification
- Formal Specification with the Java Modeling Language [preprint | Springer]
- From Specification to Proof Obligations [preprint | Springer]
- Modular Specification and Verification [preprint | Springer]
- Verifying Java Card Programs [preprint | Springer]
Part III – From Verification to Analysis
- Debugging and Visualization [preprint | Springer]
- Proof-based Test Case Generation [preprint | Springer]
- Information Flow Analysis [preprint | Springer]
- Program Transformation and Compilation [ preprint | Springer]
Part IV – The KeY System in Action
- Using the KeY Prover [preprint | Springer]
- Formal Verification with KeY: A Tutorial [preprint | Springer]
- KeY-Hoare [preprint | Springer]
Part V – Case Studies
- Verification of an Electronic Voting System [preprint | Springer]
- Verification of Counting Sort and Radix Sort [preprint | Springer]
Part VI – Appendices [Springer]
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 269, Definition 8.3
The defined tuple (pre, var, dep) must read (pre, term, dep) to be consistent with the text. var was short for variant, and term stands for termination witness.
page 321, Section 9.3.1 right before Listing 9.8
The last occurrence of
accessible before Listing 9.8 must read
KeY version from the book
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