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).


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

Last modification: 23.10.2009

Valid HTML 4.01! Valid CSS!