common sequences of events and reconfigures thesystem's code
accordingly. The optimizer also proves that correctness is preserved, i.e. that the optimized code is equivalent to the original. The improved code runs two to three times
faster than the original, and is
generated in a matter of seconds.
Senior Research Associate
PhD Fern Universitaet Hagen, 1984
My primary research interest is the
application of automated deduction to program synthesis, verification,
and optimization. Together with Bob Constable's Nuprl group and Ken
Birman's Ensemble project I currently work on formal tools and methods
for improving the performance and reliability of distributed group
communications protocols. With the Nuprl system I have built
semantics-based tools that can automatically optimize Ensemble
protocol stacks. The optimizer creates a fast-path through a stack of
I am also interested in the development
of automatic proof procedures.
Together with former students from the
Technical University of Darmstadt I
work on proof search methods based
on matrix-characterizations of logical
validity, a very compact representation
of the search space. We have
developed a uniform proof procedure
for classical logic, intuitionistic logic,
various modal logics, and fragments of
linear logic. We have also developed a
uniform algorithm for transforming the
machine-found matrix proofs into
sequent proofs, which enables us guide
the development of proofs in
interactive systems such as Nuprl. We
are currently extending this approach
to the multiplicative exponential
fragment of linear logic and inductive
theorem proving and intend to extend it
further by integrating proof planning
and similar AI techniques.
- Program Commitee: International Conference TABLEAUX'99
Review Panel: NSF Software
Engineering and Languages
- Referee: Journal of Logic and
Computation; Journal of Symbolic Computation
- Connection-based Theorem Proving in
Classical and Non-classical Logics,
Journal for Universal Computer
Science 5 (3) , (1999), 88—112 (with
- Program Synthesis. Chapter III.2.5 of
Automated Deduction — A Basis for
Applications , (1998) 105—134, Kluwer.
- Dependency Analysis Through Type
Inference. Proc. 6th Workshop on
Logic, Language, Information and
Computation , Rio de Janeiro, Brazil
(May 1999) (with O. Hafizogullari).
- Automated Fast-Track
Reconfiguration of Group
Communication Systems. Proc. 5th International Conference on Tools and
Algorithms for the Construction and
Analysis of Systems (March 1999).
- LNCS 1579, 104—118, Springer.
- A Matrix Characterization for MELL,
Proc. 6th European Workshop on Logics in Artificial Intelligence, European
Workshop (October 1998), LNAI
1489, 169—183, Springer (with H.
- Instantiation of Existentially Quantified
Variables in Inductive Specification
Proofs, Proc. 4th International
Conference on Artificial Intelligence
Computation (September 1998), LNAI 1476, 247—258,
Springer (with B. Pientka).
- A Proof Environment for the Development of Group
Communication Systems, Proc. 15th International
Conference on Automated Deduction (July 1998), LNAI
1421, 317—332, Springer (with M. Hayden and J.