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.


CompSoc Open Learning Session

27 January 2010

LINQ: Language Integrated Query in .NET

Mike Borozdin

CompSoc Open Learning Session
1830–2000 Wednesday 27 January 2010

The CompSoc open learning session this Wednesday includes a talk on LINQ, a mechanism for integrating one kind of language (database querying) into another (general object-oriented programming). This is one of the topics coming up later in APL: it’s currently a very active area of programming language development, and could be an interesting talk.

It’s bracketed by two other sessions, on singularity theory and the git version control system.

I don’t know anything more about the speaker, or even where it’s happening, because I couldn’t find that on the CompSoc site. Clues welcome.

Link: Wednesday Open Learning

Lecture 5: ESC/Java2 – The Java Extended Static Checker

25 January 2010

ESC/Java2: a verification tool combining several analysis techniques (types, dataflow, proof). An overview of the checks it performs: exception freedom for common exceptions (null pointers, array indices, class casts). The lack of soundness and completeness: false positives and defects missed. Some further and specialised annotations extending core JML (non_null, unreachable, modifies, pure). Specification inheritance.

Links: Slides; ESC/Java2 downloads.


  1. Try ESC/Java on some of the example files and some Java (1.4) programs of your own (see below how to run ESC/Java2 on DICE).
  2. Try to statically verify your previously written recipe card program with ESC/Java2.

Read the rest of this entry »

Lecture 4: JML — The Java Modeling Language

22 January 2010

Review of Hoare logic. Model-based specification as a technique for system design. Design features of JML. Some examples: preconditions, postconditions, invariants; model variables, methods and classes; ghost variables, assertions, assumptions. JML as a common language across multiple tools for software specification and verification.

Links: Slides; JML.tar.gz download.


First: please do the homework from Lecture 3! Then I can show solutions and give help in the next lecture.

Next: you must try out JML in practice by downloading and running some of the suggested tools. Try the recipe card specification homework described on the last slide from Lecture 4. It should be fun!

I recommend starting from the JML.tar.gz download described at the bottom of the JML download page. It has pre-compiled tools for several platforms. You will need a Java 1.4 runtime as well (later versions may cause difficulties). If your operating system doesn’t come with one start from Sun’s product archive.

Lecture 3: References

18 January 2010

Here are some pointers for recommended further reading and references from Lecture 3.

Read the rest of this entry »