Deductive Software Verification – The KeY Book
From Theory to Practice


Available at Springer

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.

Preprints are in many cases available on the author’s websites and linked from the table of contents below.

Table of Contents [preprint]

  1. Quo Vadis Formal Verification? [preprint | Springer]

Part I – Foundations

  1. First-Order Logic [preprint | Springer]
  2. Dynamic Logic for Java [preprint | Springer]
  3. Proof Search with Taclets [ preprint | Springer]
  4. Theories [preprint | Springer]
  5. Abstract Interpretation [preprint | Springer]

Part II – Specification and Verification

  1. Formal Specification with the Java Modeling Language [preprint | Springer]
  2. From Specification to Proof Obligations [preprint | Springer]
  3. Modular Specification and Verification [preprint | Springer]
  4. Verifying Java Card Programs [preprint | Springer]

Part III – From Verification to Analysis

  1. Debugging and Visualization [preprint | Springer]
  2. Proof-based Test Case Generation [preprint | Springer]
  3. Information Flow Analysis [preprint | Springer]
  4. Program Transformation and Compilation [ preprint | Springer]

Part IV – The KeY System in Action

  1. Using the KeY Prover [preprint | Springer]
  2. Formal Verification with KeY: A Tutorial [preprint | Springer]
  3. KeY-Hoare [preprint | Springer]

Part V – Case Studies

  1. Verification of an Electronic Voting System [preprint | Springer]
  2. Verification of Counting Sort and Radix Sort [preprint | Springer]

Part VI – Appendices [Springer]

  1. Java Modeling Language Reference [preprint]
  2. KeY File Reference [ preprint]

References [preprint]

Errata (found after publishing)

page 44, Figure 2.9
Missing closing parenthesis. The correct version is 
ε(o1, f1, singleton(o2, f2)), ε(o1, f1, allFields(o2)), and ε(o1, f1,allObjects(f2))

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 assignable.

page 554, Section 16.3.7 (Proving Termination)
In the second branch (“body preserves invariant”) of the loop rule near the bottom of the page the part d>d' in the formula should read d<d' instead.

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.