Contents

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.
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]
- 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]
- Debugging and Visualization [preprint | Springer]
- Proof-based Test Case Generation [preprint | Springer]
- Information Flow Analysis [preprint | Springer]
- Program Transformation and Compilation [ preprint | Springer]
- Using the KeY Prover [preprint | Springer]
- Formal Verification with KeY: A Tutorial [preprint | Springer]
- KeY-Hoare [preprint | Springer]
- Verification of an Electronic Voting System [preprint | Springer]
- Verification of Counting Sort and Radix Sort [preprint | Springer]
Errata (found after publishing)
page 30, Figure 2.2 The correct version of the rule eqRight should read:
accessible
before Listing 9.8 must read assignable
.