Formal semantics/Multiple inheritance
I finished a formal semantic of a C++-like language, called
CoreC++. This language is based on Jinja,
a Java-like language, developed by the
group
of Prof. Nipkow at the Technische Universitaet Muenchen. The
formalization and proof of correctness is performed in the generic
proof system Isabelle.
Verification of Slicing
Slicing, basing on control flow and program dependence graphs,
is a standard program analysis. These language independent graph
structures, together with certain well-formedness conditions,
contain enough information to perform and verify slicing.
We verify various kinds of slicing (dynamic and static intra-
as well as static interprocedural) based on these structures.
Furthermore we aim to show how different language semantics (e.g.
Jinja and CoreC++) can be embedded in these
structures, thus verifying slicing for the cores of well-known
object-oriented languages.
My Erdős number
is at most 4 (and most likely not smaller than this):
Daniel Wasserrab -> Tobias Nipkow -> Gerhard Weikum ->
Patrick Eugene O'Neil -> Paul Erdős
