Testing, Debugging and Verification - Formal Verification, part 1

Testing, Debugging, and Verification	TDA566/DIT082, LP2, HT2011
Lecture Notes, November 30.
Topics The topics of the lecture are About Formal Verification The While Language First-Order Signature Models (Kripke structures) and Program States First-Order Formulas Hoare Logic Specifying While Programs Proving Validity Symbolic Execution Symbolic State Updates Hoare Calculus with Updates Example Proof (KeY-Hoare) (Conditionals) Slides and Handouts FormalVerification1.pdf FormalVerification1-handout.pdf Examples FormalVerification2_Examples.zip (one archive for all verification lectures)

Home \| Course \| Schedule \| Exam \| Exercises \| Labs \| Evaluation \| Tools \| Links	W. Ahrendt, V. Klebanov, Dec 6, 2011