| 2026 | CAV | Consistency-Based Software Diagnosis: Accuracy, Scalability, and Limitations. | Sarah Sallinger, Lukas Graussam, Georg Weissenbacher, Florian Zuleger, Alexey Ignatiev |
| 2026 | CAV | Automated Amortised Analysis of Skew Heaps and Leftist Heaps. | Armin Walch, Georg Moser, Berry Schoenmakers, Florian Zuleger |
| 2026 | MFCS | Regular Grammars as Effective Representations of Recognizable Sets of Series-Parallel Graphs. | Marius Bozga, Radu Iosif, Florian Zuleger |
| 2025 | ESOP | Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration. | Florian Sextl, Adam Rogalewicz, Toms Vojnar, Florian Zuleger |
| 2025 | LICS | Regular Grammars for Sets of Graphs of Tree-Width 2. | Marius Bozga, Radu Iosif, Florian Zuleger |
| 2024 | IFM | Modeling Register Pairs in CompCert. | Alexander Loitzl, Florian Zuleger |
| 2024 | KR | Probabilistic Synthesis and Verification for LTL on Finite Traces. | Benjamin Aminof, Linus Cooper, Sasha Rubin, Moshe Y. Vardi, Florian Zuleger |
| 2024 | KR | Proper Linear-time Specifications of Environment Behaviors in Nondeterministic Planning and Reactive Synthesis. | Benjamin Aminof, Giuseppe De Giacomo, Sasha Rubin, Florian Zuleger |
| 2024 | LPAR | Tree-Verifiable Graph Grammars. | Mark Chimes, Radu Iosif, Florian Zuleger |
| 2024 | TACAS | Deciding Boolean Separation Logic via Small Models. | Toms Dack, Adam Rogalewicz, Toms Vojnar, Florian Zuleger |
| 2023 | CONCUR | Expressiveness Results for an Inductive Logic of Separated Relations. | Radu Iosif, Florian Zuleger |
| 2023 | LICS | Stochastic Best-Effort Strategies for Borel Goals. | Benjamin Aminof, Giuseppe De Giacomo, Sasha Rubin, Florian Zuleger |
| 2023 | LPAR | Embedding Intuitionistic into Classical Logic. | Alexander Pluska, Florian Zuleger |
| 2023 | SEFM | A Formalization of Heisenbugs and Their Causes. | Sarah Sallinger, Georg Weissenbacher, Florian Zuleger |
| 2022 | CAV | Automated Expected Amortised Cost Analysis of Probabilistic Data Structures. | Lorenz Leutgeb, Georg Moser, Florian Zuleger |
| 2022 | ECOOP | Low-Level Bi-Abduction. | Luks Holk, Petr Peringer, Adam Rogalewicz, Veronika Sokov, Toms Vojnar, Florian Zuleger |
| 2022 | IJCAI | Beyond Strong-Cyclic: Doing Your Best in Stochastic Environments. | Benjamin Aminof, Giuseppe De Giacomo, Sasha Rubin, Florian Zuleger |
| 2021 | CAV | ATLAS: Automated Amortised Complexity Analysis of Self-adjusting Data Structures. | Lorenz Leutgeb, Georg Moser, Florian Zuleger |
| 2021 | ESOP | Strong-Separation Logic. | Jens Pagel, Florian Zuleger |
| 2021 | ICCAD | Bounded Model Checking of Speculative Non-Interference. | Emmanuel Pescosta, Georg Weissenbacher, Florian Zuleger |
| 2021 | VMCAI | Eliminating Message Counters in Synchronous Threshold Automata. | Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger |
| 2020 | ATVA | Eliminating Message Counters in Threshold Automata. | Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger |
| 2020 | FMCAD | Thread-modular Counter Abstraction for Parameterized Program Safety. | Thomas Pani, Georg Weissenbacher, Florian Zuleger |
| 2020 | FOSSACS | The Polynomial Complexity of Vector Addition Systems with States. | Florian Zuleger |
| 2020 | LPAR | Beyond Symbolic Heaps: Deciding Separation Logic With Inductive Definitions. | Jens Katelaan, Florian Zuleger |
| 2020 | SAT | Multi-linear Strategy Extraction for QBF Expansion Proofs via Local Soundness. | Matthias Schlaipfer, Friedrich Slivovsky, Georg Weissenbacher, Florian Zuleger |
| 2019 | TACAS | Effective Entailment Checking for Separation Logic with Inductive Definitions. | Jens Katelaan, Christoph Matheja, Florian Zuleger |
| 2019 | TACAS | SL-COMP: Competition of Solvers for Separation Logic. | Mihaela Sighireanu, Juan Antonio Navarro Prez, Andrey Rybalchenko, Nikos Gorogiannis, Radu Iosif, Andrew Reynolds, Cristina Serban, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger, Wei-Ngan Chin, Quang Loc Le, Quang-Trung Ta, Ton-Chanh Le, Thanh-Toan Nguyen, Siau-Cheng Khoo, Michal Cyprian, Adam Rogalewicz, Toms Vojnar, Constantin Enea, Ondrej Lengl, Chong Gao, Zhilin Wu |
| 2019 | TACAS | Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking. | Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger |
| 2018 | FMCAD | Using Loop Bound Analysis For Invariant Generation. | Pavel Cadek, Clemens Danninger, Moritz Sinn, Florian Zuleger |
| 2018 | FMCAD | Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms. | Thomas Pani, Georg Weissenbacher, Florian Zuleger |
| 2018 | LICS | Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS. | Toms Brzdil, Krishnendu Chatterjee, Antonn Kucera, Petr Novotn, Dominik Velan, Florian Zuleger |
| 2018 | LPAR | Harrsh: A Tool for Unied Reasoning about Symbolic-Heap Separation Logic. | Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger |
| 2018 | PLDI | Automated clustering and program repair for introductory programming assignments. | Sumit Gulwani, Ivan Radicek, Florian Zuleger |
| 2018 | SAS | Inductive Termination Proofs with Transition Invariants and Their Relationship to the Size-Change Abstraction. | Florian Zuleger |
| 2018 | VMCAI | Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction. | Benjamin Aminof, Sasha Rubin, Ilina Stoilkovska, Josef Widder, Florian Zuleger |
| 2018 | VMCAI | From Shapes to Amortized Complexity. | Toms Fiedor, Luks Holk, Adam Rogalewicz, Moritz Sinn, Toms Vojnar, Florian Zuleger |
| 2017 | ESOP | Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic. | Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger |
| 2017 | FCT | Automata and Program Analysis. | Thomas Colcombet, Laure Daviaud, Florian Zuleger |
| 2017 | ICDT | On the Automated Verification of Web Applications with Embedded SQL. | Shachar Itzhaky, Tomer Kotek, Noam Rinetzky, Mooly Sagiv, Orr Tamir, Helmut Veith, Florian Zuleger |
| 2016 | CSL | Monadic Second Order Finite Satisfiability and Unbounded Tree-Width. | Tomer Kotek, Helmut Veith, Florian Zuleger |
| 2016 | KR | Prompt Alternating-Time Epistemic Logics. | Benjamin Aminof, Aniello Murano, Sasha Rubin, Florian Zuleger |
| 2015 | CAV | Empirical Software Metrics for Benchmarking of Verification Tools. | Yulia Demyanova, Thomas Pani, Helmut Veith, Florian Zuleger |
| 2015 | CSR | Asymptotically Precise Ranking Functions for Deterministic Size-Change Systems. | Florian Zuleger |
| 2015 | FMCAD | Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs. | Moritz Sinn, Florian Zuleger, Helmut Veith |
| 2015 | ICALP | Liveness of Parameterized Timed Networks. | Benjamin Aminof, Sasha Rubin, Florian Zuleger, Francesco Spegni |
| 2015 | LICS | Extending ALCQIO with Trees. | Tomer Kotek, Mantas Simkus, Helmut Veith, Florian Zuleger |
| 2015 | LPAR | On the Expressive Power of Communication Primitives in Parameterised Systems. | Benjamin Aminof, Sasha Rubin, Florian Zuleger |
| 2015 | PRIMA | Verification of Asynchronous Mobile-Robots in Partially-Known Environments. | Sasha Rubin, Florian Zuleger, Aniello Murano, Benjamin Aminof |
| 2014 | CAV | A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis. | Moritz Sinn, Florian Zuleger, Helmut Veith |
| 2014 | IFM | Shape and Content - A Database-Theoretic Perspective on the Analysis of Data Structures. | Diego Calvanese, Tomer Kotek, Mantas Simkus, Helmut Veith, Florian Zuleger |
| 2014 | MFCS | Size-Change Abstraction and Max-Plus Automata. | Thomas Colcombet, Laure Daviaud, Florian Zuleger |
| 2013 | FMCAD | On the concept of variable roles and its use in software analysis. | Yulia Demyanova, Helmut Veith, Florian Zuleger |
| 2013 | TACAS | Ramsey vs. Lexicographic Termination Proving. | Byron Cook, Abigail See, Florian Zuleger |
| 2011 | SAS | Bound Analysis of Imperative Programs with the Size-Change Abstraction. | Florian Zuleger, Sumit Gulwani, Moritz Sinn, Helmut Veith |
| 2010 | CADE | LOOPUS - A Tool for Computing Loop Bounds for C Programs. | Moritz Sinn, Florian Zuleger |
| 2010 | PLDI | The reachability-bound problem. | Sumit Gulwani, Florian Zuleger |
| 2009 | VMCAI | An Abstract Interpretation-Based Framework for Control Flow Reconstruction from Binaries. | Johannes Kinder, Florian Zuleger, Helmut Veith |