Dr Christoph Kreitz

CK
Contact
e-mail:

Dr. Christoph Kreitz’s research focuses on the development of logic-based formal methods and their application to the design, verification, and optimization of reliable and secure software systems. He has built logic-based tools that automatically improve the performance of fault-tolerant 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 machine-checkable 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 machine-checkable 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. 124-148, Springer 2012.

  • C. Brandt, J. Otten, C. Kreitz, W. Bibel. Specifying and Verifying Organizational Security Properties in First-Order Logic. Verification, Induction, Termination Analysis, LNCS 6463, pp. 38-53, Springer 2010.

  • T. Raths, J. Otten, C. Kreitz. The ILTP Problem Library for Intuitionistic Logic. Journal of Automated Reasoning, 38:261-271, 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):428-469, 2006.

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

  • C. Kreitz. Building Reliable, High-Performance Networks with the Nuprl Proof Development System, Journal of Functional Programming 14(1):21-68, 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 Higher-Order Logics, LNCS 2758, pp. 287-303, 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. 105-120, Springer, 2001.

  • S. Schmitt, L. Lorigo, C. Kreitz, A.Nogin. JProver: Integrating Connection-based Theorem Proving into Interactive Proof Assistants, International Joint Conference on Automated Reasoning, LNAI 2083, pp. 421-426, Springer, 2001.

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

  • X. Liu, R. van Renesse, M. Bickford, C. Kreitz, R. Constable. Protocol Switching: Exploiting Meta-Properties, International Workshop on Applied Reliable Group Communication (WARGC 2001), pp. 37-42, IEEE CS Press, 2001.

  • C. Kreitz, & B. Pientka. Connection-Driven Inductive Theorem Proving, Studia Logica 69(2):293-326, 2001.

  • C. Kreitz, J. Otten, S. Schmitt, B. Pientka. Matrix-based Constructive Theorem Proving. In Intellectics and df Computational Logic., pp. 189-205, 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. 170-176, 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. 149-160, IEEE Computer Society Press, 2000.

  • X. Liu, C. Kreitz, R. van Renesse, J. Hickey, M. Hayden, K. Birman, R. Constable. Building Reliable, High-Performance Systems from Components, Operating Systems Review 33(5):80-92, 1999.

  • C. Kreitz & J. Otten. Connection-based Theorem Proving in Classical and Non-classical Logics, Journal for Universal Computer Science 5(3):88-112, 1999.

  • C. Kreitz. Automated Fast-Track Reconfiguration of Group Communication Systems, 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1579, pp. 104-118, 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. 105-134, Kluwer, 1998.