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.
- Read more about the MRG project, and try to understand the demos. What happens when you adjust the various bits of PCC input?
- Prepare for next Monday’s lecture by reading the paper
Interfaces and specifications for the Smalltalk-80 collection classes