Mads Dam: Available degree projects
- Formal verification of the secure boot feature in a mobile trusted
module. Project on modelling and verifying part of a mobile code
platform for mobile phones using a theorem prover.
Here is a draft project description.
Company: Ericsson Research.
- Representing compositional Owicki-Gries in VCPT.
VCPT is a
theorem proving tool
to formulate and prove very general program properties. The tool can be
instantiated to different programming languages by means of an operational
semantics. Owicki-Gries is an
extension of Hoare logic to parallel imperative languages. The task is to use an operational semantics of a
suitable parallel while language represented in VCPT to derive a compositional
version of the Owicki-Gries proof system, and to validate the representation both
theoretically and practically, by example program verifications.
- The POPLmark challenge in VCPT.
The POPLmark
challenge was very recently posed as a challenge for mechanized reasoning
in the context of programming language. The challenge itself consists of a
number of generic theorems to be proved about a certain typed language
(featuring variables at both value and type levels, for connoisseurs it is
actually a typed lambda-calculus). We have reasons to believe that VCPT would
be well-suited for this kind of task. A suitable (high) level of ambition
would be to address just the first problem.
- Distributed aggregation tree protocols.
Here
is a project proposal in collaboration with Rolf Stadler at S3.
- Security protocol verification. In the advanced formal methods
course we devote some energy to verification of security protocols and the
applied pi-calculus. One suggestion is to try to verify some aspects of the
SET electronic payment protocol suite using applied pi. The SET suite is huge,
so only a small part would be considered in the project. Prior work to process
the SET specification and extract formal specifications has been done by
groups in Trento and Cambridge using the Isabelle theorem prover. This work
would provide the starting point for this project.
Last revised: 071022, Mads Dam