Christoph Kreitz

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.