Part 1     (pdf)    History, concepts and realistic program verification

Part 2a   (pdf)    Mechanical program verification

Part 2b   (pdf)    Comparison of FPP, NPPV and SPARK

Part 3a   (pdf)    FPP in more detail

Part 3b   (pdf)    Mechanical generation of invariants for FOR-loops

Part 4     (pdf)    Problems of FPP (and others), towards realistic VCs


Kauer, Stefan; Winkler, Jürgen F. H.:  A Comparison of the Program Provers NPPV and FPP.
Friedrich Schiller University, Dept. of Math. & Comp. Sci., Report Math / Inf / 99 / 28  1999Nov09  (pdf)

Kauer, Stefan; Winkler, Jürgen F. H.:  A Comparison of the Program Provers NPPV and FPP.   (pdf)
(includes all 25 (23) examples).

Freining, Carsten; Kauer, Stefan; Winkler, Jürgen F. H.:
Ein Vergleich der Programmbeweiser FPP, NPPV und SPARK   [A Comparison of the Program Provers FPP, NPPV and SPARK].
Ada-Deutschland Tagung 2002. Shaker Verlag, Aachen, 2002, 127–145.   (pdf (prelim. version))

SPARK result-protocols for the 25 (23) examples.   (pdf)

Kauer, Stefan; Winkler, Jürgen F. H.:   MechanicalGeneration of Invariants for FOR-Loops.
WING 2007, 1^st Int. Workshop on Invariant Generation, Linz/Hagenberg, 2007Jun25–26.   (pdf)

Winkler, Jürgen F. H.:  New Proof Rules for FOR-Loops.
Friedrich Schiller University, Dept. of Math. & Comp. Sci., Report Math / Inf / 98 / 13, 1998Nov07.   (pdf)

Kauer, Stefan:   Automatische Erzeugung von Verifikations- und Falsifikationsbedingungen sequentieller Programme
[Automatic Generation of Verification Conditions and Falsification Conditions of Sequential Programs].
PhD-Thesis, Friedrich Schiller University, 1999Jan27. (pdf)