An Abstract Interpretation-Based Framework for Control Flow Reconstruction from Binaries. - Johannes Kinder; Florian Zuleger; Helmut Veith (VMCAI, 2009)

LOOPUS - A Tool for Computing Loop Bounds for C Programs. - Moritz Sinn; Florian Zuleger (WING@ETAPS/IJCAR, 2010)

The reachability-bound problem. - Sumit Gulwani; Florian Zuleger (PLDI, 2010)

Bound Analysis of Imperative Programs with the Size-Change Abstraction. - Florian Zuleger; Sumit Gulwani; Moritz Sinn; Helmut Veith (SAS, 2011)

Bound Analysis of Imperative Programs with the Size-change Abstraction (extended version) - Florian Zuleger; Sumit Gulwani; Moritz Sinn; Helmut Veith (CoRR, 2012)

On the concept of variable roles and its use in software analysis. - Yulia Demyanova; Helmut Veith; Florian Zuleger (FMCAD, 2013)

Ramsey vs. Lexicographic Termination Proving. - Byron Cook; Abigail See; Florian Zuleger (TACAS, 2013)

Shape and Content: Incorporating Domain Knowledge into Shape Analysis. - Diego Calvanese; Tomer Kotek; Mantas Simkus; Helmut Veith; Florian Zuleger (Description Logics, 2014)

Towards a Description Logic for Program Analysis: Extending ALCQIO with Reachability. - Tomer Kotek; Mantas Simkus; Helmut Veith; Florian Zuleger (Description Logics, 2014)

Shape and Content - A Database-Theoretic Perspective on the Analysis of Data Structures. - Diego Calvanese; Tomer Kotek; Mantas Simkus; Helmut Veith; Florian Zuleger (IFM, 2014)

Size-Change Abstraction and Max-Plus Automata. - Thomas Colcombet; Laure Daviaud; Florian Zuleger (MFCS (1), 2014)

Extending ALCQIO with reachability. - Tomer Kotek; Mantas Simkus; Helmut Veith; Florian Zuleger (CoRR, 2014)

Asymptotically Precise Ranking Functions for Deterministic Size-Change Systems. - Florian Zuleger (CSR, 2015)

Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs. - Moritz Sinn; Florian Zuleger; Helmut Veith (FMCAD, 2015)

Liveness of Parameterized Timed Networks. - Benjamin Aminof; Sasha Rubin; Florian Zuleger; Francesco Spegni (ICALP (2), 2015)

Extending ALCQIO with Trees. - Tomer Kotek; Mantas Simkus; Helmut Veith; Florian Zuleger (LICS, 2015)

On the Expressive Power of Communication Primitives in Parameterised Systems. - Benjamin Aminof; Sasha Rubin; Florian Zuleger (LPAR, 2015)

Verification of Asynchronous Mobile-Robots in Partially-Known Environments. - Sasha Rubin; Florian Zuleger; Aniello Murano; Benjamin Aminof (PRIMA, 2015)

Loop Patterns in C Programs. - Thomas Pani; Helmut Veith; Florian Zuleger (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2015)

Automatic Verification of Multi-Agent Systems in Parameterised Grid-Environments. - Benjamin Aminof; Aniello Murano; Sasha Rubin; Florian Zuleger (AAMAS, 2016)

Monadic Second Order Finite Satisfiability and Unbounded Tree-Width. - Tomer Kotek; Helmut Veith; Florian Zuleger (CSL, 2016)

Prompt Alternating-Time Epistemic Logics. - Benjamin Aminof; Aniello Murano; Sasha Rubin; Florian Zuleger (KR, 2016)

A simple and scalable static analysis for bound analysis and amortized complexity analysis. - Moritz Sinn; Florian Zuleger; Helmut Veith (Software Engineering, 2016)

Feedback generation for performance problems in introductory programming assignments. - Florian Zuleger; Ivan Radicek; Sumit Gulwani (Software Engineering, 2016)

Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic. - Christina Jansen; Jens Katelaan; Christoph Matheja; Thomas Noll 001; Florian Zuleger (ESOP, 2017)

Automata and Program Analysis. - Thomas Colcombet; Laure Daviaud; Florian Zuleger (FCT, 2017)

On the Automated Verification of Web Applications with Embedded SQL. - Shachar Itzhaky; Tomer Kotek; Noam Rinetzky; Mooly Sagiv; Orr Tamir; Helmut Veith; Florian Zuleger (ICDT, 2017)

Systematic Predicate Abstraction Using Variable Roles. - Yulia Demyanova; Philipp Rümmer; Florian Zuleger (NFM, 2017)

Ranking Functions for Vector Addition Systems. - Florian Zuleger (CoRR, 2017)

Resource Bound Analysis (Dagstuhl Seminar 17291). - Marco Gaboardi; Jan Hoffmann 002; Reinhard Wilhelm; Florian Zuleger (Dagstuhl Reports, 2017)

Empirical software metrics for benchmarking of verification tools. - Yulia Demyanova; Thomas Pani; Helmut Veith; Florian Zuleger (Formal Methods Syst. Des., 2017)

Complexity and Resource Bound Analysis of Imperative Programs Using Difference Constraints. - Moritz Sinn; Florian Zuleger; Helmut Veith (J. Autom. Reason., 2017)

Using Loop Bound Analysis For Invariant Generation. - Pavel Cadek; Clemens Danninger; Moritz Sinn; Florian Zuleger (FMCAD, 2018)

Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms. - Thomas Pani; Georg Weissenbacher; Florian Zuleger (FMCAD, 2018)

Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS. - Tomás Brázdil; Krishnendu Chatterjee; Antonín Kucera 001; Petr Novotný 001; Dominik Velan; Florian Zuleger (LICS, 2018)

Harrsh: A Tool for Unied Reasoning about Symbolic-Heap Separation Logic. - Jens Katelaan; Christoph Matheja; Thomas Noll 001; Florian Zuleger (LPAR (Workshop and Short Papers), 2018)

Automated clustering and program repair for introductory programming assignments. - Sumit Gulwani; Ivan Radicek; Florian Zuleger (PLDI, 2018)

Inductive Termination Proofs with Transition Invariants and Their Relationship to the Size-Change Abstraction. - Florian Zuleger (SAS, 2018)

Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction. - Benjamin Aminof; Sasha Rubin; Ilina Stoilkovska; Josef Widder; Florian Zuleger (VMCAI, 2018)

From Shapes to Amortized Complexity. - Tomás Fiedor; Lukás Holík; Adam Rogalewicz; Moritz Sinn; Tomás Vojnar; Florian Zuleger (VMCAI, 2018)

Monadic refinements for relational cost analysis. - Ivan Radicek; Gilles Barthe; Marco Gaboardi; Deepak Garg 001; Florian Zuleger (Proc. ACM Program. Lang., 2018)

Effective Entailment Checking for Separation Logic with Inductive Definitions. - Jens Katelaan; Christoph Matheja; Florian Zuleger (TACAS (2), 2019)

SL-COMP: Competition of Solvers for Separation Logic. - Mihaela Sighireanu; Juan Antonio Navarro Pérez; Andrey Rybalchenko; Nikos Gorogiannis; Radu Iosif; Andrew Reynolds 001; Cristina Serban; Jens Katelaan; Christoph Matheja; Thomas Noll 001; Florian Zuleger; Wei-Ngan Chin; et al. (TACAS (3), 2019)

Eliminating Message Counters in Threshold Automata. - Ilina Stoilkovska; Igor Konnov 001; Josef Widder; Florian Zuleger (ATVA, 2020)

Thread-modular Counter Abstraction for Parameterized Program Safety. - Thomas Pani; Georg Weissenbacher; Florian Zuleger (FMCAD, 2020)

The Polynomial Complexity of Vector Addition Systems with States. - Florian Zuleger (FoSSaCS, 2020)

Beyond Symbolic Heaps: Deciding Separation Logic With Inductive Definitions. - Jens Katelaan; Florian Zuleger (LPAR, 2020)

Multi-linear Strategy Extraction for QBF Expansion Proofs via Local Soundness. - Matthias Schlaipfer; Friedrich Slivovsky; Georg Weissenbacher; Florian Zuleger (SAT, 2020)

Complete Entailment Checking for Separation Logic with Inductive Definitions. - Jens Pagel; Christoph Matheja; Florian Zuleger (CoRR, 2020)

ATLAS: Automated Amortised Complexity Analysis of Self-adjusting Data Structures. - Lorenz Leutgeb; Georg Moser; Florian Zuleger (CAV (2), 2021)

Bounded Model Checking of Speculative Non-Interference. - Emmanuel Pescosta; Georg Weissenbacher; Florian Zuleger (ICCAD, 2021)

Eliminating Message Counters in Synchronous Threshold Automata. - Ilina Stoilkovska; Igor Konnov 001; Josef Widder; Florian Zuleger (VMCAI, 2021)

Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. - Thomas Pani; Georg Weissenbacher; Florian Zuleger (Formal Methods Syst. Des., 2021)

Automated Expected Amortised Cost Analysis of Probabilistic Data Structures. - Lorenz Leutgeb; Georg Moser; Florian Zuleger (CAV (2), 2022)

Low-Level Bi-Abduction. - Lukás Holík; Petr Peringer; Adam Rogalewicz; Veronika Soková; Tomás Vojnar; Florian Zuleger (ECOOP, 2022)

Beyond Strong-Cyclic: Doing Your Best in Stochastic Environments. - Benjamin Aminof; Giuseppe De Giacomo; Sasha Rubin; Florian Zuleger (IJCAI, 2022)

Verification of agent navigation in partially-known environments. - Benjamin Aminof; Aniello Murano; Sasha Rubin; Florian Zuleger (Artif. Intell., 2022)

On the Expressiveness of a Logic of Separated Relations. - Radu Iosif; Florian Zuleger (CoRR, 2022)

Low-Level Bi-Abduction (Artifact). - Lukás Holík; Petr Peringer; Adam Rogalewicz; Veronika Soková; Tomás Vojnar; Florian Zuleger (Dagstuhl Artifacts Ser., 2022)

Verifying safety of synchronous fault-tolerant algorithms by bounded model checking. - Ilina Stoilkovska; Igor Konnov 001; Josef Widder; Florian Zuleger (Int. J. Softw. Tools Technol. Transf., 2022)

Strong-separation Logic. - Jens Pagel; Florian Zuleger (ACM Trans. Program. Lang. Syst., 2022)

Type-based analysis of logarithmic amortised complexity. - Martin Hofmann 001; Lorenz Leutgeb; David Obwaller; Georg Moser; Florian Zuleger (Math. Struct. Comput. Sci., 2022)

Algorithmenerkennung und Programmreparatur mittels Dynamischer Programmanalyse. - Florian Zuleger (ABP, 2023)

Expressiveness Results for an Inductive Logic of Separated Relations. - Radu Iosif; Florian Zuleger (CONCUR, 2023)

Stochastic Best-Effort Strategies for Borel Goals. - Benjamin Aminof; Giuseppe De Giacomo; Sasha Rubin; Florian Zuleger (LICS, 2023)

Embedding Intuitionistic into Classical Logic. - Alexander Pluska; Florian Zuleger (LPAR, 2023)

A Formalization of Heisenbugs and Their Causes. - Sarah Sallinger; Georg Weissenbacher; Florian Zuleger (SEFM, 2023)

Sound One-Phase Shape Analysis with Biabduction. - Florian Sextl; Adam Rogalewicz; Tomás Vojnar; Florian Zuleger (CoRR, 2023)

Characterizations of Definable Context-Free Graphs. - Radu Iosif; Florian Zuleger (CoRR, 2023)

The Treewidth Boundedness Problem for an Inductive Separation Logic of Relations. - Marius Bozga; Lucas Bueri; Radu Iosif; Florian Zuleger (CoRR, 2023)

A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions. - Christoph Matheja; Jens Pagel; Florian Zuleger (ACM Trans. Comput. Log., 2023)

Deciding Boolean Separation Logic via Small Models: Artifact. - Tomás Dacík; Adam Rogalewicz; Tomás Vojnar; Florian Zuleger (Zenodo, 2023)

Modeling Register Pairs in CompCert. - Alexander Loitzl; Florian Zuleger (IFM, 2024)

Probabilistic Synthesis and Verification for LTL on Finite Traces. - Benjamin Aminof; Linus Cooper; Sasha Rubin; Moshe Y. Vardi; Florian Zuleger (KR, 2024)

Proper Linear-time Specifications of Environment Behaviors in Nondeterministic Planning and Reactive Synthesis. - Benjamin Aminof; Giuseppe De Giacomo; Sasha Rubin; Florian Zuleger (KR, 2024)

Tree-Verifiable Graph Grammars. - Mark Chimes; Radu Iosif; Florian Zuleger (LPAR, 2024)

Deciding Boolean Separation Logic via Small Models. - Tomás Dacík; Adam Rogalewicz; Tomás Vojnar; Florian Zuleger (TACAS (1), 2024)

Effective MSO-Definability for Tree-width Bounded Models of an Inductive Separation Logic of Relations. - Lucas Bueri; Radu Iosif; Florian Zuleger (CoRR, 2024)

Deciding Boolean Separation Logic via Small Models (Technical Report). - Tomás Dacík; Adam Rogalewicz; Tomás Vojnar; Florian Zuleger (CoRR, 2024)

Regular Grammars for Graph Sets of Tree-Width ≤. - Marius Bozga; Radu Iosif; Florian Zuleger (CoRR, 2024)

Deciding Boolean Separation Logic via Small Models: Artifact. - Tomás Dacík; Adam Rogalewicz; Tomás Vojnar; Florian Zuleger (Zenodo, 2024)

Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification. - Thomas Pani; Georg Weissenbacher; Florian Zuleger (Formal Methods Syst. Des., 2024)

Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration. - Florian Sextl; Adam Rogalewicz; Tomás Vojnar; Florian Zuleger (ESOP (2), 2025)

Parameterized Model-checking of Discrete-Timed Networks and Symmetric-Broadcast Systems. - Benjamin Aminof; Sasha Rubin; Francesco Spegni; Florian Zuleger (Log. Methods Comput. Sci., 2025)

Artifact for "Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration". - Florian Sextl; Adam Rogalewicz; Tomás Vojnar; Florian Zuleger (Zenodo, 2025)

Artifact for "Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration". - Florian Sextl; Adam Rogalewicz; Tomás Vojnar; Florian Zuleger (Zenodo, 2025)