Proof-Carrying Code (Lab)

Prof. Dr. Heiko Mantel
please contact Ms. Kraft (S2|02/E318)
will be announced during the preparation meeting
Preparation Meeting:
Wednesday, April 13, 2011, 16:30 in S2|02/A213
Weekly date:
Wednesday, 14:25–16:05 in S2|02/E306
Markus Aderhold


For a given piece of software, it is in general hard to assess if it satisfies the properties that the manufacturer promises. If these properties are defined formally, then formal methods can be used to verify whether the software satisfies the properties.

The idea behind proof-carrying code is to include formal proofs in software. While the construction of proofs is often difficult and usually requires creativity, checking the proofs can be done automatically. In this way, the receiver of proof-carrying code can convince himself/herself that the software indeed satisfies the desired properties.

The goal of this lab course is to realize the proof-carrying code concept within a Java-based framework. This means that the framework itself is implemented in Java, while the software to be checked is given as Java bytecode. A case study shall demonstrate the practical usability of this framework.

Technically, the framework uses a client-server infrastructure. The clients are mobile devices such as cell phones or PDAs. Since these devices have only limited resources to check the proofs, the framework needs to be designed in a way that proof checking gets sufficiently simple.

The lab course belongs to the area Foundations of Computing (Modulhandbucheintrag) and can be taken in conjunction with the seminar on proof-carrying code in the same semester.


  • programming skills in Java
  • mandatory courses of the first four semesters in the Computer Science program

Here is the link to the internal web page.

Last modified on 21 April 2011.

A A A | Print | Imprint | Sitemap | Contact
zum Seitenanfang