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
certificates
- 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
class
- The Bill class together with the
certificate
- 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.