Jochen Hoenicke

Jochen Hoenicke University of Freiburg Georges-Köhler-Allee 52 79110 Freiburg   building 052, room 00-020 +49 761 203 82431 hoenicke@informatik.uni-freiburg.de2 jochen-hoenicke.de3

Research Interests

program verification, invariant generation for sequential and concurrent programs, interpolation in SMT; timed automata, duration calculus, model-checking.

Projects

• SmtInterpol⁴
• Ultimate⁵
• VerisoftXT⁶
• AVACS⁷

Publications

• Jürgen Christ and Jochen Hoenicke. Proof Tree Preserving Tree Interpolation. Journal of Automated Reasoning, 57(1):67–95, June 2016. [doi⁸]
• Jochen Hoenicke and Andreas Podelski. Fairness for Infinitary Control. In Correct System Design – Symposium in Honor of Ernst-Rüdiger Olderog. 2015. [doi⁹]
• Azadeh Farzan, Matthias Heizmann, Jochen Hoenicke, Zachary Kincaid and Andreas Podelski. Automated Program Verification. In LATA 2015. 2015. [doi¹⁰]
• Jürgen Christ and Jochen Hoenicke. Cutting the Mix. In CAV 2015. 2015. [doi¹¹]
• Jürgen Christ and Jochen Hoenicke. Weakly Equivalent Arrays. In FroCos 2015. 2015. [doi¹²] The author's version is available at arXiv¹³.
• Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. Termination Analysis by Learning Terminating Programs. In CAV 2014. Springer, 2014. [doi¹⁴]
• Matthias Heizmann, Jochen Hoenicke, Jan Leike, and Andreas Podelski. Linear Ranking for Linear Lasso Programs. In ATVA 2013, volume 8172 in LNCS, pages 365–380. Springer, 2013. [doi¹⁵] The author's version is available at arXiv¹⁶.
• Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. Software Model Checking for People Who Love Automata. In CAV 2013, volume 8044 in LNCS, pages 36–52. Springer, 2013. Invited tutorial. [doi¹⁷]
• Jürgen Christ and Jochen Hoenicke. Extending Proof Tree Preserving Interpolation to Sequences and Trees. In SMT-workshop. 2013. [pdf¹⁸]
• Jürgen Christ, Jochen Hoenicke, and Alexander Nutz. Proof Tree Preserving Interpolation. In TACAS 13, volume 7795 in LNCS, pages 126–140. Springer, 2013. [doi¹⁹ | technical report ²⁰| improved version²¹]
• Jürgen Christ, Jochen Hoenicke, and Alexander Nutz. SMTInterpol: An Interpolating SMT Solver. In Model Checking Software, volume 7385 in LNCS, pages 248–254. Springer, 2012. [doi²² | pdf²³]
• A. Post and J. Hoenicke. Formalization and analysis of real-time requirements: a feasibility study at BOSCH. In VSTTE 12, LNCS, pages 225-240. Springer, 2012. [ bib²⁴ | doi²⁵ | .pdf²⁶ ]
• E. Ermis, J. Hoenicke, and A. Podelski. Splitting via interpolants. In VMCAI 12, LNCS, pages 186-201. Springer, 2012. [ bib²⁴ | doi²⁷ | .pdf²⁸ ]
• A. Post, J. Hoenicke, and A. Podelski. Vacuous real-time requirements. In RE 11, pages 153-162. IEEE, 2011. [ bib²⁴ | doi²⁹ | .pdf³⁰ ]
• A. Post, J. Hoenicke, and A. Podelski. rt-inconsistency: a new property for real-time requirements. In FASE 2011, number 6603 in LNCS, pages 34-49. Springer, 2011. [ bib³¹ | doi³² | .pdf³³ ]
• J. Hoenicke, K.R.M. Leino, A. Podelski, M. Schäf, and T. Wies. Doomed program points. Formal Methods in System Design, 37(2-3):171-199, December 2010. [ bib²⁴ | doi³⁴ ]
• J. Hoenicke, R. Meyer, and E.-R. Olderog. Kleene, Rabin, and Scott are available. In CONCUR 2010, number 6269 in LNCS, pages 462-477. Springer, 2010. [ bib³⁵ | doi³⁶ | .pdf³⁷ ]
  
• J. Hoenicke, E.-R. Olderog, and A. Podelski. Fairness for dynamic control. In TACAS 2010, number 6015 in LNCS, pages 251-265. Springer, 2010. [ bib³⁸ | doi³⁹ | .pdf⁴⁰ ]
  
• M. Heizmann, J. Hoenicke, and A. Podelski. Nested interpolants. In POPL 10, pages 471-482. ACM, 2010. [ bib⁴¹ | doi⁴² | .pdf⁴³ ]
• J. Hoenicke, K.R.M. Leino, A. Podelski, M. Schäf, and T. Wies. It's doomed; we can prove it. In FM 2009, number 5850 in LNCS, pages 338-353. Springer, 2009. [ bib⁴⁴ | doi⁴⁵ | .pdf⁴⁶ ]
• M. Heizmann, J. Hoenicke, and A. Podelski. Refinement of trace abstraction. In Static Analysis Symposium (SAS 2009), number 5673 in LNCS, pages 69-85. Springer, 2009. [ bib⁴⁷ | doi⁴⁸ | .pdf⁴⁹ ]
  
• R. Meyer, J. Faber, J. Hoenicke, and A. Rybalchenko. Model checking Duration Calculus: a practical approach. Formal Aspects of Computing, 20(4-5):481-505, July 2008. [ bib⁵⁰ | doi⁵¹ ]
• Jochen Hoenicke. Combination of Processes, Data, and Time. PhD thesis, University of Oldenburg, July 2006. [ bib⁵² | .pdf⁵³ ]
• Jochen Hoenicke and Patrick Maier. Model-checking of specifications integrating processes, data and time. In J.S. Fitzgerald, I.J. Hayes, and A. Tarlecki, editors, FM 2005, volume 3582 of LNCS, pages 465-480. Springer, 2005. [ bib⁵⁴ | doi⁵⁵ | .pdf⁵⁶ ]
• J. Hoenicke and E.-R. Olderog. CSP-OZ-DC: A combination of specification techniques for processes, data and time. Nordic Journal of Computing, 9(4):301-334, 2002. appeared March 2003. [ bib ⁵⁷ | .pdf⁵⁸ ]
• J. Hoenicke and E.-R. Olderog. Combining Specification Techniques for Processes Data and Time. In M. Butler, L. Petre, and K. Sere, editors, Integrated Formal Methods, volume 2335 of Lecture Notes in Computer Science, pages 245-266. Springer-Verlag, May 2002. [ bib⁵⁹ | doi⁶⁰ | .pdf⁶¹ ]
• J. Hoenicke. Specification of Radio Based Railway Crossings with the Combination of CSP, OZ, and DC. FBT 2001, June 2001. [ bib⁶² | .pdf⁶³ ]

Conferences

I am on the program committee of Boogie 2012⁶⁴.