Publications

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]

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]