Jochen Hoenicke

62 papers A* 4A 9B 11C 1Journal 18Unranked 18

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	A lazy and modular approach to int-blasting. Acta Informatica Max Barth, Matthias Heizmann, Jochen Hoenicke
2026	—	`conf`	On the Power of Temporal Prophecy. On the Pursuit of Insight and Elegance Jochen Hoenicke, Oded Padon, Sharon Shoham
2023	A	`conf`	Choose Your Colour: Tree Interpolation for Quantified Formulas in SMT. CADE Elisabeth Henkel, Jochen Hoenicke, Tanja Schindler
2023	J	`jnl`	Choose your Colour: Tree Interpolation for Quantified Formulas in SMT. CoRR Elisabeth Henkel, Jochen Hoenicke, Tanja Schindler
2023	—	`conf`	Ultimate Automizer and the CommuHash Normal Form - (Competition Contribution). TACAS (2) Matthias Heizmann, Max Barth, Daniel Dietsch, Leonard Fichtner, Jochen Hoenicke, Dominik Klumpp, Mehdi Naouar, Tanja Schindler, Frank Schüssele, Andreas Podelski
2022	—	`conf`	A Simple Proof Format for SMT. SMT Jochen Hoenicke, Tanja Schindler
2021	B	`conf`	Incremental Search for Conflict and Unit Instances of Quantified Formulas with E-Matching. VMCAI Jochen Hoenicke, Tanja Schindler
2021	—	`conf`	Proof Tree Preserving Sequence Interpolation of Quantified Formulas in the Theory of Equality. SMT Elisabeth Henkel, Jochen Hoenicke, Tanja Schindler
2021	—	`conf`	Separating Map Variables in a Logic-Based Intermediate Verification Language. NETYS Daniel Dietsch, Matthias Heizmann, Jochen Hoenicke, Alexander Nutz, Andreas Podelski
2021	J	`jnl`	Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems. CoRR Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham
2021	J	`jnl`	Temporal prophecy for proving temporal properties of infinite-state systems. Formal Methods Syst. Des. Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham
2019	J	`jnl`	Different Maps for Different Uses. A Program Transformation for Intermediate Verification Languages. CoRR Daniel Dietsch, Matthias Heizmann, Jochen Hoenicke, Alexander Nutz, Andreas Podelski
2019	J	`jnl`	Interpolation and the Array Property Fragment. CoRR Jochen Hoenicke, Tanja Schindler
2019	A	`conf`	Scalable Analysis of Real-Time Requirements. RE Vincent Langenfeld, Daniel Dietsch, Bernd Westphal, Jochen Hoenicke, Amalinda Post
2019	B	`conf`	Solving and Interpolating Constant Arrays Based on Weak Equivalences. VMCAI Jochen Hoenicke, Tanja Schindler
2019	—	`conf`	Ultimate TreeAutomizer (CHC-COMP Tool Description). HCVS/PERR@ETAPS Daniel Dietsch, Matthias Heizmann, Jochen Hoenicke, Alexander Nutz, Andreas Podelski
2018	—	`conf`	A Tree-Based Approach to Data Flow Proofs. VSTTE Jochen Hoenicke, Alexander Nutz, Andreas Podelski
2018	A	`conf`	Efficient Interpolation for the Theory of Arrays. IJCAR Jochen Hoenicke, Tanja Schindler
2018	J	`jnl`	Efficient Interpolation for the Theory of Arrays. CoRR Jochen Hoenicke, Tanja Schindler
2018	J	`jnl`	Reducing liveness to safety in first-order logic. Proc. ACM Program. Lang. Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, Sharon Shoham
2018	B	`conf`	Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems. FMCAD Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham
2018	—	`conf`	The Map Equality Domain. VSTTE Daniel Dietsch, Matthias Heizmann, Jochen Hoenicke, Alexander Nutz, Andreas Podelski
2018	—	`conf`	Ultimate Automizer and the Search for Perfect Interpolants - (Competition Contribution). TACAS (2) Matthias Heizmann, Yu-Fang Chen, Daniel Dietsch, Marius Greitschus, Jochen Hoenicke, Yong Li, Alexander Nutz, Betim Musa, Christian Schilling, Tanja Schindler, Andreas Podelski
2018	—	`conf`	Ultimate Taipan with Dynamic Block Encoding - (Competition Contribution). TACAS (2) Daniel Dietsch, Marius Greitschus, Matthias Heizmann, Jochen Hoenicke, Alexander Nutz, Andreas Podelski, Christian Schilling, Tanja Schindler
2017	—	`conf`	Efficient Interpolation for the Theory of Arrays. SMT Jochen Hoenicke, Tanja Schindler
2017	J	`jnl`	Proof Tree Preserving Interpolation. CoRR Jürgen Christ, Jochen Hoenicke, Alexander Nutz
2017	A*	`conf`	Thread modularity at many levels: a pearl in compositional verification. POPL Jochen Hoenicke, Rupak Majumdar, Andreas Podelski
2016	J	`jnl`	Proof Tree Preserving Tree Interpolation. J. Autom. Reason. Jürgen Christ, Jochen Hoenicke
2015	C	`conf`	Automated Program Verification. LATA Azadeh Farzan, Matthias Heizmann, Jochen Hoenicke, Zachary Kincaid, Andreas Podelski
2015	—	`conf`	Cutting the Mix. CAV (2) Jürgen Christ, Jochen Hoenicke
2015	—	`conf`	Fairness for Infinitary Control. Correct System Design Jochen Hoenicke, Andreas Podelski
2015	—	`conf`	Weakly Equivalent Arrays. FroCos Jürgen Christ, Jochen Hoenicke
2014	J	`jnl`	Linear Ranking for Linear Lasso Programs. CoRR Matthias Heizmann, Jochen Hoenicke, Jan Leike, Andreas Podelski
2014	A*	`conf`	Termination Analysis by Learning Terminating Programs. CAV Matthias Heizmann, Jochen Hoenicke, Andreas Podelski
2014	J	`jnl`	Termination Analysis by Learning Terminating Programs. CoRR Matthias Heizmann, Jochen Hoenicke, Andreas Podelski
2014	A	`conf`	Ultimate Automizer with Unsatisfiable Cores - (Competition Contribution). TACAS Matthias Heizmann, Jürgen Christ, Daniel Dietsch, Jochen Hoenicke, Markus Lindenmann, Betim Musa, Christian Schilling, Stefan Wissert, Andreas Podelski
2014	A	`conf`	Ultimate Kojak - (Competition Contribution). TACAS Evren Ermis, Alexander Nutz, Daniel Dietsch, Jochen Hoenicke, Andreas Podelski
2014	—	`conf`	Weakly Equivalent Arrays. SMT Jürgen Christ, Jochen Hoenicke
2014	J	`jnl`	Weakly Equivalent Arrays. CoRR Jürgen Christ, Jochen Hoenicke
2013	B	`conf`	Linear Ranking for Linear Lasso Programs. ATVA Matthias Heizmann, Jochen Hoenicke, Jan Leike, Andreas Podelski
2013	A	`conf`	Proof Tree Preserving Interpolation. TACAS Jürgen Christ, Jochen Hoenicke, Alexander Nutz
2013	A*	`conf`	Software Model Checking for People Who Love Automata. CAV Matthias Heizmann, Jochen Hoenicke, Andreas Podelski
2013	A	`conf`	Ultimate Automizer with SMTInterpol - (Competition Contribution). TACAS Matthias Heizmann, Jürgen Christ, Daniel Dietsch, Evren Ermis, Jochen Hoenicke, Markus Lindenmann, Alexander Nutz, Christian Schilling, Andreas Podelski
2012	J	`jnl`	Automotive behavioral requirements expressed in a specification pattern system: a case study at BOSCH. Requir. Eng. Amalinda Post, Igor Menzel, Jochen Hoenicke, Andreas Podelski
2012	—	`conf`	Formalization and Analysis of Real-Time Requirements: A Feasibility Study at BOSCH. VSTTE Amalinda Post, Jochen Hoenicke
2012	—	`conf`	SMTInterpol: An Interpolating SMT Solver. SPIN Jürgen Christ, Jochen Hoenicke, Alexander Nutz
2012	B	`conf`	Splitting via Interpolants. VMCAI Evren Ermis, Jochen Hoenicke, Andreas Podelski
2012	J	`jnl`	Towards Bounded Infeasible Code Detection CoRR Jürgen Christ, Jochen Hoenicke, Martin Schäf
2011	A	`conf`	Vacuous real-time requirements. RE Amalinda Post, Jochen Hoenicke, Andreas Podelski
2011	B	`conf`	rt-Inconsistency: A New Property for Real-Time Requirements. FASE Amalinda Post, Jochen Hoenicke, Andreas Podelski
2010	J	`jnl`	Doomed program points. Formal Methods Syst. Des. Jochen Hoenicke, K. Rustan M. Leino, Andreas Podelski, Martin Schäf, Thomas Wies
2010	A	`conf`	Fairness for Dynamic Control. TACAS Jochen Hoenicke, Ernst-Rüdiger Olderog, Andreas Podelski
2010	—	`conf`	Instantiation-Based Interpolation for Quantified Formulae. Decision Procedures in Software, Hardware and Bioware Jürgen Christ, Jochen Hoenicke
2010	B	`conf`	Kleene, Rabin, and Scott Are Available. CONCUR Jochen Hoenicke, Roland Meyer, Ernst-Rüdiger Olderog
2010	A*	`conf`	Nested interpolants. POPL Matthias Heizmann, Jochen Hoenicke, Andreas Podelski
2009	B	`conf`	It's Doomed; We Can Prove It. FM Jochen Hoenicke, K. Rustan M. Leino, Andreas Podelski, Martin Schäf, Thomas Wies
2009	B	`conf`	Refinement of Trace Abstraction. SAS Matthias Heizmann, Jochen Hoenicke, Andreas Podelski
2008	J	`jnl`	Model checking Duration Calculus: a practical approach. Formal Aspects Comput. Roland Meyer, Johannes Faber, Jochen Hoenicke, Andrey Rybalchenko
2006	—	`—`	Combination of processes, data, and time. Jochen Hoenicke
2005	B	`conf`	Model-Checking of Specifications Integrating Processes, Data and Time. FM Jochen Hoenicke, Patrick Maier
2002	J	`jnl`	CSP-OZ-DC: A Combination of Specification Techniques for Processes, Data and Time. Nord. J. Comput. Jochen Hoenicke, Ernst-Rüdiger Olderog
2002	B	`conf`	Combining Specification Techniques for Processes, Data and Time. IFM Jochen Hoenicke, Ernst-Rüdiger Olderog