You are here: Home Team Jürgen Christ

Jürgen Christ




I received my Ph.D. from the Chair of Software Engineering, Institute of Computer Science, University of Freiburg. My research includes SMT solving, Craig interpolation, and invariant generation.  As of November 1, 2015 I left academia.



  • Interpolation Modulo Theories, Dissertation [PDF]
  • Weakly Equivalent Arrays, with Jochen Hoenicke in SMT 2014 [extended version]
  • Extending Proof Tree Preserving Interpolation to Sequences and Trees, with Jochen Hoenicke in SMT 2013 [PDF]
  • Proof Tree Preserving Interpolation, with Jochen Hoenicke, and Alexander Nutz in TACAS 2013 [Technical Report]
  • Flow-sensitive Fault Localization, with Evren Ermis, Martin Schäf, and Thomas Wies in VMCAI 2013 [PDF]
  • SMTInterpol: An Interpolating SMT Solver, with Alexander Nutz and Jochen Hoenicke in SPIN 2012 [PDF]
  • Instantiation-Based Interpolation for Quantified Formulae, with Jochen Hoenicke in SMT 2010 [PDF (Color), PDF (Black and White)]



Consultation Hours

  • By appointment