Program Synthesis, Verification, and Transformation
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.

BACK
Back to main page
Related Sites
Synthesis Systems Research Groups People Conferences / Journals Misc.
Nuprl ftp
Nuprl 5
MetaPRL
HOL
PVS
VSE
Isabelle
Verifix
LEDA
PopLog
Cyclone

Cornell CS
NuPRL (Cornell)
Ensemble (Cornell)
Ensemble-Nuprl
Kestrel Institute
NASA Ames   ASE
Isabelle (Cambridge)
Isabelle (Munich)
Logical Frameworks
Project I/O Automata
DOVE: Design Oriented Verification and Evaluation
BBN UAV
KeY Project
ISIS Vanderbilt



Ken Birman
Bob Constable
Karl Crary
Jason Hickey
Dieter Hutter
Mike Lowry
Lawrence Paulson
Benjamin Pierce
John Rushby
Peter Sewell
Doug Smith
Robbert Van Renesse
ASE
LICS
FroCos (2000)
LoPSTR
FME
ALL Conferences
ASE JFP
JSC

DARPA ITO
Compulog






Abstract Formale Methoden der künstlichen Intelligenz
Künstliche Intelligenz, 2007. 		PS Version PDF Version
Abstract Building Reliable, High-Performance Networks with the Nuprl Proof Development System
Journal of Functional Programming, 2004. 		PS Version PDF Version
Abstract User-specified Adaptive Scheduling in a Streaming Media Network.
Technical Report, Cornell University, 2002. 		PS Version PDF Version
Abstract Proving Hybrid Protocols Correct
TPHOLs 2001, 2001. 		PS Version PDF Version
Abstract Formally Verifying Hybrid Protocols with the Nuprl Logical Programming Environment
Technical Report, Cornell University, 2001. 		PS Version PDF Version
Abstract An Experiment in Formal Design using Meta-Properties
DISCEX II, 2001. 		PS Version PDF Version
Abstract Protocol Switching: Exploiting Meta-Properties
WARGC 2001, 2001. 		PS Version PDF Version
Abstract The Horus and Ensemble Projects: Accomplishments and Limitations.
DISCEX'00, 2000. 		PS Version PDF Version
Abstract Building Reliable, High-Performance Systems from Components.
SOSP'99, 1999. 		PS Version PDF Version
Abstract Dependence Analysis Through Type Inference.
WoLLIC'99, 1999. 		PS Version PDF Version
Abstract Automated Fast-Track Reconfiguration of Group Communication Systems.
TACAS 99, 1999. 		PS Version PDF Version
Abstract Formal Reasoning about Communication Systems II: Automated Fast-Track Reconfiguration.
Technical Report, Cornell University, 1998. 		PS Version PDF Version
Abstract A Type-based Framework for Automatic Debugging
Technical Report, Cornell University, 1998. 		PS Version PDF Version
Abstract Dead Code Elimination Through Type Inference
Technical Report, Cornell University, 1998. 		PS Version PDF Version
Abstract A Proof Environment for the Development of Group Communication Systems.
CADE-15, 1998. 		PS Version PDF Version
Abstract Program Synthesis.
In Automated Deduction - A Basis for Applications, Kluwer, 1998. 		PS Version PDF Version
Abstract A multi-level approach to program synthesis.
LoPSTr'97, 1998. 		PS Version PDF Version
Abstract Formal Reasoning about Communication Systems I: Embedding ML into Type Theory.
Technical Report, Cornell University, 1997. 		PS Version PDF Version
Abstract Formal Reasoning about Modules, Reuse, Objects, and their Correctness.
FAPR'96, 1996. 		PS Version PDF Version
Abstract Formal Mathematics for Verifiably Correct Program Synthesis.
Journal of the IGPL, 1996. 		PS Version PDF Version
Abstract Logical Foundations for Declarative Object-oriented Programming
Technical Report, TU Darmstadt, 1995. 		PS Version PDF Version
Abstract A Foundation for Verified Software Development Systems.
Technical Report, TU Darmstadt, 1994. 		PS Version PDF Version
Abstract Metasynthesis - Deriving Programs that Develop Programs.
Thesis for Habilitation, TU Darmstadt, 1992. 		PS Version PDF Version
Abstract Deriving Strategies for the Design of Global Search Algorithms.
Technical Report, TU Darmstadt, 1992. 		PS Version PDF Version
Abstract Towards a formal theory of program construction.
Revue d' Intelligence Artificielle, 1990. 		PS Version PDF Version
Abstract The representation of program synthesis in higher order logic.
GWAI-90, 1990. 		PS Version PDF Version
Abstract XPRTS - an implementation tool for program synthesis.
GWAI-89, 1989. 		Not available online
Abstract Logic Oriented Program Synthesis - goals and realization.
Technical Report, TU München, 1988. 		PS Version PDF Version
Abstract Towards a flexible LOPS implementation: an example of XPRTS programming.
Technical Report, TU München, 1987. 		PS Version PDF Version
BACK
Back to main page