1998 - 1999 CS Annual Report                                                        Researchers
choices.gif (4488 bytes)


Christoph Kreitz

Senior Research Associate

kreitz@cs.cornell.edu
http://www.cs.cornell.edu/home/kreitz

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 protocols for 
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. 

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. 

Professional Activities 

  • Program Commitee: International Conference TABLEAUX'99  
  • Review Panel: NSF Software Engineering and Languages 
  • Referee: Journal of Logic and Computation; Journal of Symbolic Computation
Publications 
  • Connection-based Theorem Proving in Classical and Non-classical Logics, Journal for Universal Computer Science 5 (3) , (1999), 88—112 (with J. Otten). 
  • 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. Mantel). 
  • Instantiation of Existentially Quantified Variables in Inductive Specification Proofs, Proc. 4th International Conference on Artificial Intelligence and Symbolic  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. Hickey).