Lecture 6: Certifying correctness

28 January 2010

Verification at different levels (design, specification, implementation) and horizontal/vertical translations (refinement, optimisation, compilation). Forms of certification and example approaches: proof-carrying code, translation validation and compiler correctness.

I mentioned some example research projects which have (hopefully!) working demos.

Links: Slides; research projects: MRG, Mobius, Compcert.

Homework