Dr Christoph Kreitz
Kestrel Institute 3260 Hillview Avenue Palo Alto CA 94304 U.S.A.

Dr. Christoph Kreitz’s research focuses on the development of logicbased formal methods and their application to the design, verification, and optimization of reliable and secure software systems. He has built logicbased tools that automatically improve the performance of faulttolerant communication systems and guarantee that the improvements do not introduce errors. He also works on enhancing the automatic reasoning capabilities of tactical theorem provers such as Nuprl, Coq, and Isabelle and has developed machinecheckable proofs for the proof obligations in Specware’s library.
He is interested in using his expertise in theorem proving and formal methods to help formally specify network protocols, develop code generation strategies, and develop strategies for the creation of machinecheckable proofs that verify the properties of the generated implementations.
Selected Publications:

C. Kreitz. Nuprl as Logical Framework for Automating Proofs in Category Theory, Kozen Festschrift, LNCS 7230, pp. 124148, Springer 2012.

C. Brandt, J. Otten, C. Kreitz, W. Bibel. Specifying and Verifying Organizational Security Properties in FirstOrder Logic. Verification, Induction, Termination Analysis, LNCS 6463, pp. 3853, Springer 2010.

T. Raths, J. Otten, C. Kreitz. The ILTP Problem Library for Intuitionistic Logic. Journal of Automated Reasoning, 38:261271, 2007.

S. Allen, M. Bickford, R. Constable, R. Eaton, C. Kreitz, L. Lorigo, E. Moran. Innovations in Computational Type Theory using Nuprl, Journal of Applied Logic 4(4):428469, 2006.

C. Kreitz & H. Mantel. A Matrix Characterization for Multiplicative Exponential Linear Logic, Journal of Automated Reasoning 32(2):121166, 2004.

C. Kreitz. Building Reliable, HighPerformance Networks with the Nuprl Proof Development System, Journal of Functional Programming 14(1):2168, 2004.

J. Hickey, A. Nogin, R. Constable, B.Aydemir, E. Barzilay, Y. Bryukhov, R. Eaton, A.Kopylov, C. Kreitz, V. Krupski, L. Lorigo, S. Schmitt, C.Witty, X.Yu. MetaPRL  A Modular Logical Environment, International Conference on Theorem Proving in HigherOrder Logics, LNCS 2758, pp. 287303, Springer, 2003.

M. Bickford, C. Kreitz, R. van Renesse, X. Liu. Proving Hybrid Protocols Correct, 14th International Conference on Theorem Proving in Higher Order Logics, LNCS 2152, pp. 105120, Springer, 2001.

S. Schmitt, L. Lorigo, C. Kreitz, A.Nogin. JProver: Integrating Connectionbased Theorem Proving into Interactive Proof Assistants, International Joint Conference on Automated Reasoning, LNAI 2083, pp. 421426, Springer, 2001.

M. Bickford, C. Kreitz, R. van Renesse, R. Constable. An Experiment in Formal Design using MetaProperties, DARPA Information Survivability Conference and Exposition II (DISCEX 2001), pp. 100107, IEEE Computer Society Press, 2001.

X. Liu, R. van Renesse, M. Bickford, C. Kreitz, R. Constable. Protocol Switching: Exploiting MetaProperties, International Workshop on Applied Reliable Group Communication (WARGC 2001), pp. 3742, IEEE CS Press, 2001.

C. Kreitz, & B. Pientka. ConnectionDriven Inductive Theorem Proving, Studia Logica 69(2):293326, 2001.

C. Kreitz, J. Otten, S. Schmitt, B. Pientka. Matrixbased Constructive Theorem Proving. In Intellectics and df Computational Logic., pp. 189205, Kluwer, 2000.

S. Allen, R. Constable, R. Eaton, C. Kreitz, L. Lorigo. The Nuprl Open Logical Environment, 17th International Conference on Automated Deduction, LNAI 1831, pp. 170176, Springer, 2000.

K. Birman, B. Constable, M. Hayden, J. Hickey, C. Kreitz, R. van Renesse, O. Rodeh, W.Vogels. The Horus and Ensemble Projects: Accomplishments and Limitations. DARPA Information Survivability Conference and Exposition (DISCEX 2000), pp. 149160, IEEE Computer Society Press, 2000.

X. Liu, C. Kreitz, R. van Renesse, J. Hickey, M. Hayden, K. Birman, R. Constable. Building Reliable, HighPerformance Systems from Components, Operating Systems Review 33(5):8092, 1999.

C. Kreitz & J. Otten. Connectionbased Theorem Proving in Classical and Nonclassical Logics, Journal for Universal Computer Science 5(3):88112, 1999.

C. Kreitz. Automated FastTrack Reconfiguration of Group Communication Systems, 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1579, pp. 104118, Springer, 1999.

C. Kreitz, M. Hayden, J. Hickey. A Proof Environment for the Development of Group Communication Systems, 15th International Conference on Automated Deduction, LNAI 1421, pp. 317  332, Springer, 1998.

C. Kreitz. Program Synthesis. In Automated Deduction  A Basis for Applications, Kapitel III.2.5, pp. 105134, Kluwer, 1998.