Jena University, Dept. of Math. and Computer Science, Inst. of Computer Science
Programming Languages and Compilers, Prof. J.F.H. Winkler 

Course "Mechanical Program Verification"

Budapest, ELTE, 2008.Oct.06..10

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

Part 2 (pdf)   Mechanical program verification

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

Part 3 (pdf)    FPP in more detail

Part 3a(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  1999.Nov.09   ( 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.
    Ada-Deutschland Tagung 2002. Shaker Verlag, Aachen, 2002. S. 127..145 ( pdf )

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

Kauer, Stefan; Winkler, Jürgen F. H.
MechanicalGeneration of Invariants for FOR-Loops.WING 2007, 1st 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 1998.Nov.07 (pdf)

Kauer, Stefan:
Automatische Erzeugung von Verifikations- und Falsifikationsbedingungen sequentieller Programme. Dissertation, Friedrich Schiller University, 1999.Jan.27 (pdf)


Institute | Home | Comments  |  Jürgen Winkler 2009Feb20