Andreas Podelski
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
123
Venues
33
Active years
1992–2026
Best venue rank
A*
Where they publish
- ATACAS25 papers
- A*POPL10 papers
- BSAS10 papers
- BREFSQ8 papers
- A*CAV8 papers
- BVMCAI8 papers
- ACP6 papers
- BICLP6 papers
- ARE5 papers
- A*LICS4 papers
- A*PLDI3 papers
- BCogSci3 papers
- BATVA3 papers
- BFM2 papers
- CPADL2 papers
- AESOP2 papers
- BCSL2 papers
- BFMCAD1 paper
- CTAP1 paper
- AICST1 paper
- CLATA1 paper
- A*AAAI1 paper
- CISoLA1 paper
- AISSTA1 paper
- AISSRE1 paper
- BFASE1 paper
- CICTAC1 paper
- BFOSSACS1 paper
- BSOFSEM1 paper
- BLPAR1 paper
- BMFCS1 paper
- BMFPS1 paper
- A*ICALP1 paper
Papers
123 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2026 | REFSQ | Provably Relevant HAL Interface Requirements for Embedded Systems. | Manuel Bentele, Andreas Podelski, Axel Sikora, Bernd Westphal |
| 2026 | REFSQ | A Practical and Complete Method for Detecting rt-Inconsistencies in Real-Time Requirements. | Nico Hauff, Elisabeth Henkel, Elisabeth Fnfgeld, Vincent Langenfeld, Andreas Podelski |
| 2026 | REFSQ | Automata-Represented Requirements in HanforPL - A Visual Approach for Requirements Engineering Practice and Formal Reasoning. | Tobias Kolzer, Vincent Langenfeld, Nico Hauff, Elisabeth Henkel, Andreas Podelski |
| 2026 | TACAS | Ultimate Automizer with a One-Dimensional Memory Model - (Competition Contribution). | Manuel Bentele, Max Barth, Marcel Ebbinghaus, Jan Krner, Daniel Dietsch, Matthias Heizmann, Dominik Klumpp, Frank Schssele, Andreas Podelski |
| 2025 | CAV | Counterexample-Guided Commutativity. | Marcel Ebbinghaus, Dominik Klumpp, Andreas Podelski |
| 2025 | REFSQ | Hanfor: Requirements Formalisation and Beyond. | Nico Hauff, Elisabeth Henkel, Tobias Kolzer, Vincent Langenfeld, Andreas Podelski |
| 2024 | RE | Scalable Redundancy Detection for Real-Time Requirements. | Elisabeth Henkel, Nico Hauff, Lena Funk, Vincent Langenfeld, Andreas Podelski |
| 2024 | TACAS | Ultimate Automizer and the Abstraction of Bitwise Operations - (Competition Contribution). | Frank Schssele, Manuel Bentele, Daniel Dietsch, Matthias Heizmann, Xinyu Jiang, Dominik Klumpp, Andreas Podelski |
| 2023 | REFSQ | An Empirical Study of the Intuitive Understanding of a Formal Pattern Language. | Elisabeth Henkel, Nico Hauff, Lukas Eber, Vincent Langenfeld, Andreas Podelski |
| 2023 | TACAS | Ultimate Taipan and Race Detection in Ultimate - (Competition Contribution). | Daniel Dietsch, Matthias Heizmann, Dominik Klumpp, Frank Schssele, Andreas Podelski |
| 2023 | TACAS | Ultimate Automizer and the CommuHash Normal Form - (Competition Contribution). | Matthias Heizmann, Max Barth, Daniel Dietsch, Leonard Fichtner, Jochen Hoenicke, Dominik Klumpp, Mehdi Naouar, Tanja Schindler, Frank Schssele, Andreas Podelski |
| 2022 | PLDI | Sound sequentialization for concurrent program verification. | Azadeh Farzan, Dominik Klumpp, Andreas Podelski |
| 2022 | TACAS | Ultimate GemCutter and the Axes of Generalization - (Competition Contribution). | Dominik Klumpp, Daniel Dietsch, Matthias Heizmann, Frank Schssele, Marcel Ebbinghaus, Azadeh Farzan, Andreas Podelski |
| 2021 | CogSci | A Formal Operational Model of ACT-R: Structure and Behaviour. | Vincent Langenfeld, Bernd Westphal, Andreas Podelski |
| 2021 | REFSQ | Hanfor: Semantic Requirements Review at Scale. | Samuel Becker, Daniel Dietsch, Nico Hauff, Elisabeth Henkel, Vincent Langenfeld, Andreas Podelski, Bernd Westphal |
| 2021 | VMCAI | Verification of Concurrent Programs Using Petri Net Unfoldings. | Daniel Dietsch, Matthias Heizmann, Dominik Klumpp, Mehdi Naouar, Andreas Podelski, Claus Schtzle |
| 2019 | CogSci | On Formal Verification of ACT-R Architectures and Models. | Vincent Langenfeld, Bernd Westphal, Andreas Podelski |
| 2018 | CogSci | But does it really do that? Using formal analysis to ensure desirable ACT-R model behaviour. | Vincent Langenfeld, Bernd Westphal, Rebecca Albrecht, Andreas Podelski |
| 2018 | FMCAD | Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems. | Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham |
| 2018 | TACAS | Ultimate Taipan with Dynamic Block Encoding - (Competition Contribution). | Daniel Dietsch, Marius Greitschus, Matthias Heizmann, Jochen Hoenicke, Alexander Nutz, Andreas Podelski, Christian Schilling, Tanja Schindler |
| 2018 | TACAS | Ultimate Automizer and the Search for Perfect Interpolants - (Competition Contribution). | Matthias Heizmann, Yu-Fang Chen, Daniel Dietsch, Marius Greitschus, Jochen Hoenicke, Yong Li, Alexander Nutz, Betim Musa, Christian Schilling, Tanja Schindler, Andreas Podelski |
| 2017 | POPL | Thread modularity at many levels: a pearl in compositional verification. | Jochen Hoenicke, Rupak Majumdar, Andreas Podelski |
| 2017 | SAS | Loop Invariants from Counterexamples. | Marius Greitschus, Daniel Dietsch, Andreas Podelski |
| 2017 | TACAS | Ultimate Taipan: Trace Abstraction and Abstract Interpretation - (Competition Contribution). | Marius Greitschus, Daniel Dietsch, Matthias Heizmann, Alexander Nutz, Claus Schtzle, Christian Schilling, Frank Schssele, Andreas Podelski |
| 2017 | TACAS | Ultimate Automizer with an On-Demand Construction of Floyd-Hoare Automata - (Competition Contribution). | Matthias Heizmann, Yu-Wen Chen, Daniel Dietsch, Marius Greitschus, Alexander Nutz, Betim Musa, Claus Schtzle, Christian Schilling, Frank Schssele, Andreas Podelski |
| 2016 | LICS | Proving Liveness of Parameterized Programs. | Azadeh Farzan, Zachary Kincaid, Andreas Podelski |
| 2016 | REFSQ | Requirements Defects over a Project Lifetime: An Empirical Analysis of Defect Data from a 5-Year Automotive Project at Bosch. | Vincent Langenfeld, Amalinda Post, Andreas Podelski |
| 2016 | TACAS | Ultimate Automizer with Two-track Proofs - (Competition Contribution). | Matthias Heizmann, Daniel Dietsch, Marius Greitschus, Jan Leike, Betim Musa, Claus Schtzle, Andreas Podelski |
| 2016 | TAP | Classifying Bugs with Interpolants. | Andreas Podelski, Martin Schf, Thomas Wies |
| 2015 | CAV | Fairness Modulo Theory: A New Approach to LTL Software Model Checking. | Daniel Dietsch, Matthias Heizmann, Vincent Langenfeld, Andreas Podelski |
| 2015 | ICST | If A Fails, Can B Still Succeed? Inferring Dependencies between Test Results in Automotive System Testing. | Stephan Arlt, Tobias Morciniec, Andreas Podelski, Silke Wagner |
| 2015 | LATA | Automated Program Verification. | Azadeh Farzan, Matthias Heizmann, Jochen Hoenicke, Zachary Kincaid, Andreas Podelski |
| 2015 | POPL | Proof Spaces for Unbounded Parallelism. | Azadeh Farzan, Zachary Kincaid, Andreas Podelski |
| 2015 | RE | Using the requirements specification to infer the implicit test status of requirements. | Tobias Morciniec, Andreas Podelski |
| 2015 | TACAS | Ultimate Automizer with Array Interpolation - (Competition Contribution). | Matthias Heizmann, Daniel Dietsch, Jan Leike, Betim Musa, Andreas Podelski |
| 2015 | TACAS | ULTIMATE KOJAK with Memory Safety Checks - (Competition Contribution). | Alexander Nutz, Daniel Dietsch, Mostafa Mahmoud Mohamed, Andreas Podelski |
| 2014 | AAAI | Planning as Model Checking in Hybrid Domains. | Sergiy Bogomolov, Daniele Magazzeni, Andreas Podelski, Martin Wehrle |
| 2014 | CAV | Termination Analysis by Learning Terminating Programs. | Matthias Heizmann, Jochen Hoenicke, Andreas Podelski |
| 2014 | ISoLA | Verification of GUI Applications: A Black-Box Approach. | Stephan Arlt, Evren Ermis, Sergio Feo-Arenis, Andreas Podelski |
| 2014 | ISSTA | Reducing GUI test suites via program slicing. | Stephan Arlt, Andreas Podelski, Martin Wehrle |
| 2014 | POPL | Proofs that count. | Azadeh Farzan, Zachary Kincaid, Andreas Podelski |
| 2014 | TACAS | Ultimate Kojak - (Competition Contribution). | Evren Ermis, Alexander Nutz, Daniel Dietsch, Jochen Hoenicke, Andreas Podelski |
| 2014 | TACAS | Ultimate Automizer with Unsatisfiable Cores - (Competition Contribution). | Matthias Heizmann, Jrgen Christ, Daniel Dietsch, Jochen Hoenicke, Markus Lindenmann, Betim Musa, Christian Schilling, Stefan Wissert, Andreas Podelski |
| 2014 | TACAS | Quasi-Equal Clock Reduction: More Networks, More Queries. | Christian Herrera, Bernd Westphal, Andreas Podelski |
| 2013 | ATVA | Linear Ranking for Linear Lasso Programs. | Matthias Heizmann, Jochen Hoenicke, Jan Leike, Andreas Podelski |
| 2013 | CAV | Software Model Checking for People Who Love Automata. | Matthias Heizmann, Jochen Hoenicke, Andreas Podelski |
| 2013 | POPL | Inductive data flow graphs. | Azadeh Farzan, Zachary Kincaid, Andreas Podelski |
| 2013 | TACAS | Ultimate Automizer with SMTInterpol - (Competition Contribution). | Matthias Heizmann, Jrgen Christ, Daniel Dietsch, Evren Ermis, Jochen Hoenicke, Markus Lindenmann, Alexander Nutz, Christian Schilling, Andreas Podelski |
| 2013 | VMCAI | Automata as Proofs. | Andreas Podelski |
| 2012 | ATVA | Interpolant Automata - (Invited Talk). | Andreas Podelski |
| 2012 | CAV | A Box-Based Distance between Regions for Guiding the Reachability Analysis of SpaceEx. | Sergiy Bogomolov, Goran Frehse, Radu Grosu, Hamed Ladan, Andreas Podelski, Martin Wehrle |
| 2012 | ISSRE | Lightweight Static Analysis for GUI Testing. | Stephan Arlt, Andreas Podelski, Cristiano Bertolini, Martin Schf, Ishan Banerjee, Atif M. Memon |
| 2012 | RE | Towards successful subcontracting for software in small to medium-sized enterprises. | Bernd Westphal, Daniel Dietsch, Sergio Feo-Arenis, Andreas Podelski, Louis Pahlow, Jochen Morsbach, Barbara Sommer, Anke Fuchs, Christine Meierhfer |
| 2012 | VMCAI | Splitting via Interpolants. | Evren Ermis, Jochen Hoenicke, Andreas Podelski |
| 2011 | FASE | rt-Inconsistency: A New Property for Real-Time Requirements. | Amalinda Post, Jochen Hoenicke, Andreas Podelski |
| 2011 | FM | System Verification through Program Verification. | Daniel Dietsch, Bernd Westphal, Andreas Podelski |
| 2011 | RE | Disambiguation of industrial standards through formalization and graphical languages. | Daniel Dietsch, Sergio Feo-Arenis, Bernd Westphal, Andreas Podelski |
| 2011 | RE | Vacuous real-time requirements. | Amalinda Post, Jochen Hoenicke, Andreas Podelski |
| 2011 | REFSQ | Applying Restricted English Grammar on Automotive Requirements - Does it Work? A Case Study. | Amalinda Post, Igor Menzel, Andreas Podelski |
| 2011 | TACAS | Transition Invariants and Transition Predicate Abstraction for Program Termination. | Andreas Podelski, Andrey Rybalchenko |
| 2010 | ATVA | Composing Reachability Analyses of Hybrid Systems for Safety and Stability. | Sergiy Bogomolov, Corina Mitrohin, Andreas Podelski |
| 2010 | POPL | Nested interpolants. | Matthias Heizmann, Jochen Hoenicke, Andreas Podelski |
| 2010 | POPL | Counterexample-guided focus. | Andreas Podelski, Thomas Wies |
| 2010 | SAS | Size-Change Termination and Transition Invariants. | Matthias Heizmann, Neil D. Jones, Andreas Podelski |
| 2010 | SAS | Thread-Modular Counterexample-Guided Abstraction Refinement. | Alexander Malkis, Andreas Podelski, Andrey Rybalchenko |
| 2010 | TACAS | Fairness for Dynamic Control. | Jochen Hoenicke, Ernst-Rdiger Olderog, Andreas Podelski |
| 2009 | FM | It's Doomed; We Can Prove It. | Jochen Hoenicke, K. Rustan M. Leino, Andreas Podelski, Martin Schf, Thomas Wies |
| 2009 | SAS | Refinement of Trace Abstraction. | Matthias Heizmann, Jochen Hoenicke, Andreas Podelski |
| 2009 | SAS | Abstraction Refinement for Quantified Array Assertions. | Mohamed Nassim Seghir, Andreas Podelski, Thomas Wies |
| 2009 | TACAS | Transition-Based Directed Model Checking. | Martin Wehrle, Sebastian Kupferschmid, Andreas Podelski |
| 2008 | CAV | Faster Than Uppaal? | Sebastian Kupferschmid, Martin Wehrle, Bernhard Nebel, Andreas Podelski |
| 2008 | CAV | Heap Assumptions on Demand. | Andreas Podelski, Andrey Rybalchenko, Thomas Wies |
| 2008 | VMCAI | Is Lazy Abstraction a Decision Procedure for Broadcast Protocols? | Rayna Dimitrova, Andreas Podelski |
| 2007 | PADL | ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement. | Andreas Podelski, Andrey Rybalchenko |
| 2007 | PLDI | Proving thread termination. | Byron Cook, Andreas Podelski, Andrey Rybalchenko |
| 2007 | POPL | Proving that programs eventually do something good. | Byron Cook, Alexey Gotsman, Andreas Podelski, Andrey Rybalchenko, Moshe Y. Vardi |
| 2007 | SAS | Precise Thread-Modular Verification. | Alexander Malkis, Andreas Podelski, Andrey Rybalchenko |
| 2007 | TACAS | Uppaal/DMC- Abstraction-Based Heuristics for Directed Model Checking. | Sebastian Kupferschmid, Klaus Drger, Jrg Hoffmann, Bernd Finkbeiner, Henning Dierks, Andreas Podelski, Gerd Behrmann |
| 2006 | CAV | Terminator: Beyond Safety. | Byron Cook, Andreas Podelski, Andrey Rybalchenko |
| 2006 | ICTAC | Thread-Modular Verification Is Cartesian Abstract Interpretation. | Alexander Malkis, Andreas Podelski, Andrey Rybalchenko |
| 2006 | PLDI | Termination proofs for systems code. | Byron Cook, Andreas Podelski, Andrey Rybalchenko |
| 2006 | VMCAI | Field Constraint Analysis. | Thomas Wies, Viktor Kuncak, Patrick Lam, Andreas Podelski, Martin C. Rinard |
| 2005 | ESOP | Summaries for While Programs with Recursion. | Andreas Podelski, Ina Schaefer, Silke Wagner |
| 2005 | POPL | Transition predicate abstraction and fair termination. | Andreas Podelski, Andrey Rybalchenko |
| 2005 | SAS | Abstraction Refinement for Termination. | Byron Cook, Andreas Podelski, Andrey Rybalchenko |
| 2005 | SAS | Boolean Heaps. | Andreas Podelski, Thomas Wies |
| 2005 | TACAS | Separating Fairness and Well-Foundedness for the Analysis of Fair Discrete Systems. | Amir Pnueli, Andreas Podelski, Andrey Rybalchenko |
| 2004 | CP | Constraints in Program Analysis and Verification. | Andreas Podelski |
| 2004 | LICS | Transition Invariants. | Andreas Podelski, Andrey Rybalchenko |
| 2004 | VMCAI | A Complete Method for the Synthesis of Linear Ranking Functions. | Andreas Podelski, Andrey Rybalchenko |
| 2003 | FOSSACS | Verification of Cryptographic Protocols: Tagging Enforces Termination. | Bruno Blanchet, Andreas Podelski |
| 2003 | VMCAI | Software Model Checking with Abstraction Refinement. | Andreas Podelski |
| 2002 | ICLP | Constraint-Based Infinite Model Checking and Tabulation for Stratified CLP. | Witold Charatonik, Supratik Mukhopadhyay, Andreas Podelski |
| 2002 | TACAS | Relative Completeness of Abstraction Refinement for Software Model Checking. | Thomas Ball, Andreas Podelski, Sriram K. Rajamani |
| 2002 | VMCAI | Compositional Termination Analysis of Symbolic Forward Analysis. | Witold Charatonik, Supratik Mukhopadhyay, Andreas Podelski |
| 2001 | PADL | Constraint Database Models Characterizing Timed Bisimilarity. | Supratik Mukhopadhyay, Andreas Podelski |
| 2001 | SOFSEM | Model Checking Communication Protocols. | Pablo Argn, Giorgio Delzanno, Supratik Mukhopadhyay, Andreas Podelski |
| 2001 | TACAS | Boolean and Cartesian Abstraction for Model Checking C Programs. | Thomas Ball, Andreas Podelski, Sriram K. Rajamani |
| 2000 | POPL | Paths vs. Trees in Set-Based Program Analysis. | Witold Charatonik, Andreas Podelski, Jean-Marc Talbot |
| 2000 | POPL | Efficient Algorithms for pre | Javier Esparza, Andreas Podelski |
| 2000 | SAS | Model Checking as Constraint Solving. | Andreas Podelski |
| 1999 | CSL | Constraint-Based Analysis of Broadcast Protocols. | Giorgio Delzanno, Javier Esparza, Andreas Podelski |
| 1999 | ESOP | Set-Based Failure Analysis for Logic Programs and Concurrent Constraint Programs. | Andreas Podelski, Witold Charatonik, Martin Mller |
| 1999 | TACAS | Model Checking in CLP. | Giorgio Delzanno, Andreas Podelski |
| 1998 | LICS | The Horn Mu-calculus. | Witold Charatonik, David A. McAllester, Damian Niwinski, Andreas Podelski, Igor Walukiewicz |
| 1998 | SAS | Directional Type Inference for Logic Programs. | Witold Charatonik, Andreas Podelski |
| 1998 | TACAS | Set-Based Analysis of Reactive Infinite-State Systems. | Witold Charatonik, Andreas Podelski |
| 1997 | CP | Ordering Constraints over Feature Trees. | Martin Mller, Joachim Niehren, Andreas Podelski |
| 1997 | CP | Set Constraints: A Pearl in Research on Constraints. | Leszek Pacholski, Andreas Podelski |
| 1997 | CSL | LISA: A Specification Language Based on WS2S. | Abdelwaheb Ayari, David A. Basin, Andreas Podelski |
| 1997 | LICS | Set Constraints with Intersection. | Witold Charatonik, Andreas Podelski |
| 1996 | CP | The Independence Property of a Class of Set Constraints. | Witold Charatonik, Andreas Podelski |
| 1995 | CP | A Detailed Algorithm Testing Guards over Feature Trees. | Andreas Podelski, Peter Van Roy |
| 1995 | CP | Situated Simplification. | Andreas Podelski, Gert Smolka |
| 1995 | ICLP | Operational Semantics of Constraint Logic Programs with Coroutining. | Andreas Podelski, Gert Smolka |
| 1995 | ICLP | Situated Simplification. | Andreas Podelski, Gert Smolka |
| 1993 | ICLP | Order-Sorted Feature Theory Unification. | Hassan At-Kaci, Andreas Podelski, Seth Copen Goldstein |
| 1993 | ICLP | An Informal Introduction to LIFE. | Hassan At-Kaci, Andreas Podelski, Peter Van Roy |
| 1993 | ICLP | The Beauty and the Beast Algorithm: Testing Entailment and Disentailment Incrementally. | Andreas Podelski, Peter Van Roy |
| 1993 | LPAR | Entailment and Disentailment of Order-Sorted Feature Constraints. | Hassan At-Kaci, Andreas Podelski |
| 1993 | MFCS | Rabin Tree Automata and Finite Monoids. | Danile Beauquier, Andreas Podelski |
| 1993 | MFPS | Ultimately Periodic Words of Rational | Hugues Calbrix, Maurice Nivat, Andreas Podelski |
| 1992 | ICALP | On Reverse and General Definite Tree Languages (Extended Abstract). | Pierre Pladeau, Andreas Podelski |