Deductive Software Verification – The KeY Book
From Theory to Practice

bookcover

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:

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.