Umbra: case study

In order to verify the applicability of the BML tools we developed a small case study in which we excercised the existing tool set.

The whole case study materials include:

  1. A bundle with jars which package PCC certificates
  2. A bundle with source code of the Demonstrator application together with the JML specifications
  3. A bundle with Demonstrator jars augmented with BML specifications
  4. A bundle with the Coq proofs for the Bill class
  5. The Bill class together with the certificate
  6. A bundle with jars that unpack the certificate and verify its correctness against the code which arrived

A paper which summarises the case study is available here (PDF).

Contact

If you want to contact the authors of the tool, please send an email to Aleksy Schubert or Jacek Chrz±szcz.