My primary research interest is the design and implementation of logical
formalisms and knowledge-based techniques for the development of reliable and
efficient software. My main focus in this area is the application of automated deduction to program synthesis,
verification, and optimization.
In my former work at the Technical Universities of München and Darmstadt
I have implemented logical program synthesis tools and developed a formal
logical foundation for knowledge-based program construction.
My current research at Cornell aims at a logical programming
environment for the construction of high-confidence distributed systems.
In cooperation with the
Nuprl and
Ensemble research groups
I have built semantics-based formal tools that can automatically optimize
protocol stacks of the Ensemble group communication system. The tools create
a fast-path through a stack of communication protocols for common sequences of
operation, reconfigure the system's code accordingly, and give a Nuprl proof
of the correctness of the optimizations. The optimized code performs two to
three times faster than the original one.
|
Most of my publications in the area of
Program Synthesis, Verification, and Transformation are available online in
postscript or PDF format. An abstract with a complete reference and
corresponding bibtex entry is also provided. Unix tar files of my program
transformation tools can be downloaded from this page.
A list of related web pages is given to simplify cross references.
|
|