Laura Kovacs,
"Automated Invariant Generation by Algebraic Techniques for Imperative Program Verification in Theorema"
, Serie RISC, Johannes Kepler University Linz, Austria, 10-2007
Original Titel:
Automated Invariant Generation by Algebraic Techniques for Imperative Program Verification in Theorema