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:
- A bundle with jars which package PCC
- A bundle with source code of the
Demonstrator application together with the JML specifications
- A bundle with Demonstrator jars augmented with BML specifications
- A bundle with the Coq proofs for the Bill
- The Bill class together with the
- 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
Last modification: 23.10.2009