Publications

go next top of page

Publications

[HPS24]
Jochen Hoenicke, Oded Padon, and Sharon Shoham. On the Power of Temporal Prophecy. In PODELSKI 65. Springer, 2024. [abstract]
[HHS23]
Elisabeth Henkel, Jochen Hoenicke, and Tanja Schindler. Choose Your Colour: Tree Interpolation for Quantified Formulas in SMT. In CADE 2023, pages 248–265. Springer, 2023. [doi | preprint with proofs | abstract]
[HS22]
Jochen Hoenicke and Tanja Schindler. A Simple Proof Format for SMT. In SMT 2022, pages 54–70. CEUR-WS.org, 2022. [pdf | abstract]
[DHHNP21]
Daniel Dietsch, Matthias Heizmann, Jochen Hoenicke, Alexander Nutz, and Andreas Podelski. Separating Map Variables in a Logic-Based Intermediate Verification Language. In NETYS, pages 169–186. Springer, 2021. [doi | abstract]
[PHMPSS21]
Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, and Sharon Shoham. Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems. Formal Methods in System Design, 57(2):246–269, July 2021. [doi | abstract]
[HHS21]
Elisabeth Henkel, Jochen Hoenicke, and Tanja Schindler. Proof Tree Preserving Sequence Interpolation of Quantified Formulas in the Theory of Equality. In SMT 2021, pages 3–16. CEUR-WS.org, 2021. [pdf | abstract]
[HS21]
Jochen Hoenicke and Tanja Schindler. Incremental Search for Conflict and Unit Instances of Quantified Formulas with E-Matching. In VMCAI 2021, pages 534–555. Springer, 2021. [doi | abstract]
[LDWHP19]
Vincent Langenfeld, Daniel Dietsch, Bernd Westphal, Jochen Hoenicke, and Amalinda Post. Scalable Analysis of Real-Time Requirements. In RE 2019, pages 234–244. Springer, 2019. [doi | abstract]
[HS19]
Jochen Hoenicke and Tanja Schindler. Solving and Interpolating Constant Arrays Based on Weak Equivalences. In VMCAI 2019, pages 297–317. Springer, 2019. [doi | abstract]
[DHHNP18]
Daniel Dietsch, Matthias Heizmann, Jochen Hoenicke, Alexander Nutz, and Andreas Podelski. Ultimate TreeAutomizer (CHC-COMP Tool Description). In HCVS/PERR@ETAPS 2019, volume 296 in EPTCS, pages 42–47. 2019. [doi | pdf | abstract]
[HS19a]
Jochen Hoenicke and Tanja Schindler. Interpolation and the Array Property Fragment. In CoRR abs/1904.11381. arXiv, 2019. [pdf | abstract]
[PHMPSS18]
Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham. Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems. In FMCAD 18. IEEE, 2018. [doi | pdf | abstract]
[DHHNP18]
Daniel Dietsch, Matthias Heizmann, Jochen Hoenicke, Alexander Nutz, and Andreas Podelski. The Map Equality Domain. In VSTTE 18, pages 291–308. Springer, 2018. [doi | abstract]
[HNP18]
Jochen Hoenicke, Alexander Nutz, and Andreas Podelski. A Tree-based Approach to Data Flow Proofs. In VSTTE 18, pages 1–16. Springer, 2018. [doi | abstract]
[HS18]
Jochen Hoenicke and Tanja Schindler. Efficient Interpolation for the Theory of Arrays. In IJCAR 18, pages 549–565. Springer, 2018. [doi | abstract] The author's version is available at arXiv.
[DGHHNPSS18]
Daniel Dietsch, Marius Greitschus, Matthias Heizmann, Jochen Hoenicke, Alexander Nutz, Andreas Podelski, Christian Schilling, and Tanja Schindler. Ultimate Taipan with Dynamic Block Encoding – (Competition Contribution). In TACAS (2) 18, pages 452–456. Springer, 2018. [doi | abstract]
[HCDGHLNMSSP18]
Matthias Heizmann, Yu-Fang Chen, Daniel Dietsch, Marius Greitschus, Jochen Hoenicke, Yong Li, Alexander Nutz, Betim Musa, Christian Schilling, Tanja Schindler, and Andreas Podelski. Ultimate Automizer and the Search for Perfect Interpolants – (Competition Contribution). In TACAS (2) 18, pages 447–451. Springer, 2018. [doi | abstract]
[PHLPS18]
Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, and Sharon Shoham. Reducing Liveness to Safety in First-order Logic. In PACMPL 2 (POPL), pages 26:1–26:33. ACM, 2018. [doi | abstract]
[HMP17]
Jochen Hoenicke, Rupak Majumdar, and Andreas Podelski. Thread Modularity at Many Levels: a pearl in compositional verification. In POPL 17, pages 473–485. ACM, 2017. [doi | abstract]
[CH16]
Jürgen Christ and Jochen Hoenicke. Proof Tree Preserving Tree Interpolation. Journal of Automated Reasoning, 57(1):67–95, June 2016. [doi | abstract]
[HP15]
Jochen Hoenicke and Andreas Podelski. Fairness for Infinitary Control. In Correct System Design – Symposium in Honor of Ernst-Rüdiger Olderog. 2015. [doi | abstract]
[FHHKP15]
Azadeh Farzan, Matthias Heizmann, Jochen Hoenicke, Zachary Kincaid and Andreas Podelski. Automated Program Verification. In LATA 2015. 2015. [doi | abstract]
[CH15]
Jürgen Christ and Jochen Hoenicke. Cutting the Mix. In CAV 2015. 2015. [doi | abstract]
[CH14]
Jürgen Christ and Jochen Hoenicke. Weakly Equivalent Arrays. In FroCos 2015. 2015. [doi | abstract] The author's version is available at arXiv.
[HHP14]
Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. Termination Analysis by Learning Terminating Programs. In CAV 2014. Springer, 2014. [doi | abstract]
[HHLP13]
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 | abstract] The author's version is available at arXiv.
[HHP13]
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 | abstract]
[CH13]
Jürgen Christ and Jochen Hoenicke. Extending Proof Tree Preserving Interpolation to Sequences and Trees. In SMT-workshop. 2013. [pdf | abstract]
[CHN13]
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 | abstract] The author's version is available at arXiv.
[CHN12]
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 | abstract]
[PH12]
Amalinda Post and Jochen Hoenicke. Formalization and Analysis of Real-Time Requirements: a Feasibility Study at BOSCH. In VSTTE 12, pages 225–240. Springer, 2012. [doi | pdf | abstract]
[EHP12]
Evren Ermis, Jochen Hoenicke, and Andreas Podelski. Splitting via Interpolants. In VMCAI 12, pages 186–201. Springer, 2012. [doi | pdf | abstract]
[PHP11b]
Amalinda Post, Jochen Hoenicke, and Andreas Podelski. Vacuous real-time requirements. In RE 11, pages 153–162. IEEE, 2011. [doi | pdf | abstract]
[PHP11]
Amalinda Post, Jochen Hoenicke, and Andreas Podelski. rt-inconsistency: a new property for real-time requirements. In FASE 2011, volume 6603 in LNCS, pages 34–49. Springer, 2011. [doi | pdf | abstract]
[HLPSW10]
Jochen Hoenicke, K. Rustan M. Leino, Andreas Podelski, Martin Schäf, and Thomas Wies. Doomed Program Points. Formal Methods in System Design, 37(2–3):171–199, December 2010. [doi | abstract]
[HMO10]
Jochen Hoenicke, Roland Meyer, and E.-R. Olderog. Kleene, Rabin, and Scott are available. In CONCUR 2010, volume 6269 in LNCS, pages 462–477. Springer, 2010. [doi | pdf | abstract]
[HOP10]
Jochen Hoenicke, E.-R. Olderog, and Andreas Podelski. Fairness for Dynamic Control. In TACAS 2010, volume 6015 in LNCS, pages 251–265. Springer, 2010. [doi | pdf | abstract]
[HHP10]
Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. Nested Interpolants. In POPL 10, pages 471–482. ACM, 2010. [doi | pdf | abstract]
[HLPSW09]
Jochen Hoenicke, K. Rustan M. Leino, Andreas Podelski, Martin Schäf, and Thomas Wies. It's Doomed; we can Prove it. In FM 2009, volume 5850 in LNCS, pages 338–353. Springer, 2009. [doi | pdf | abstract]
[HHP09]
Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. Refinement of Trace Abstraction. In Static Analysis Symposium (SAS 2009), volume 5673 in LNCS, pages 69–85. Springer, 2009. [doi | pdf | abstract]
[MFHR08]
Roland Meyer, Johannes Faber, Jochen Hoenicke, and Andrey Rybalchenko. Model Checking Duration Calculus: a practical approach. Formal Aspects of Computing, 20(4–5):481–505, July 2008. [doi | abstract]
[HM05]
Jochen Hoenicke and Patrick Maier. Model-Checking of Specifications Integrating Processes, Data and Time. In FM 2005, volume 3582 in LNCS, pages 465–480. Springer, 2005. [doi | pdf | abstract]
[HO02b]
Jochen Hoenicke and Ernst-Rüdiger 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. [pdf | abstract]
[HO02a]
Jochen Hoenicke and Ernst-Rüdiger Olderog. Combining Specification Techniques for Processes Data and Time. In Integrated Formal Methods, volume 2335 in Lecture Notes in Computer Science, pages 245–266. Springer, May 2002. [doi | pdf | abstract]
[Hoe01]
Jochen Hoenicke. Specification of Radio Based Railway Crossings with the Combination of CSP, OZ, and DC. FBT 2001, jun 2001. [pdf | abstract]
 top of page go back

Thesis

[Hoe06]
Jochen Hoenicke. Combination of Processes, Data, and Time. PhD thesis, University of Oldenburg, July 2006. [pdf | abstract]
[Hoe99]
Jochen Hoenicke. Graphische Spezifikationsspachen: Der Zusammenhang zwischen Constraint Diagrams und Real-Time Symbolic Timing Diagrams. Master's thesis, University of Oldenburg, 1999. In German. [pdf | abstract]