Formal semantics
I am currently working on a formal semantics for a large subset of Java
including threads for both source and byte code. The semantics is based
on the Jinja semantics by T. Nipkow und G. Klein and is formalised in the
theorem prover
Isabelle/HOL.
For both the source code and byte code sematnics type safety is to be
shown. Moreover, part of it is also a compiler to be formalized and
verified that translates source code programs to observationally
equivalent byte code programs.
The formalisation in progress is available for download in the
Archive of Formal Proofs
with project title Jinja with Threads.
Temporal path conditions
I also work on temporal path conditions for paths in program and system
dependence graphs. They improve on boolean path conditions, which are used
to make slicing more precise: By allowing to express temporal
relationsships, they are more precise. By connecting them to a model
checker, they are used to automatically generate "witness"
traces for information flow along a specific path.
