Florian Zuleger

112 papers A* 11A 8B 24C 3Misc 1Journal 47Unranked 18

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	Characterizations of Monadic Second Order Definable Context-Free Sets of Graphs. Log. Methods Comput. Sci. Radu Iosif, Florian Zuleger
2025	—	`conf`	Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration. ESOP (2) Florian Sextl, Adam Rogalewicz, Tomás Vojnar, Florian Zuleger
2025	—	`conf`	Iterating Non-Aggregative Structure Compositions. FSTTCS Marius Bozga, Radu Iosif, Florian Zuleger
2025	J	`jnl`	Iterating Non-Aggregative Structure Compositions. CoRR Marius Bozga, Radu Iosif, Florian Zuleger
2025	J	`jnl`	Parameterized Model-checking of Discrete-Timed Networks and Symmetric-Broadcast Systems. Log. Methods Comput. Sci. Benjamin Aminof, Sasha Rubin, Francesco Spegni, Florian Zuleger
2025	A*	`conf`	Regular Grammars for Sets of Graphs of Tree-Width 2. LICS Marius Bozga, Radu Iosif, Florian Zuleger
2025	J	`jnl`	To Zip Through the Cost Analysis of Probabilistic Programs. CoRR Matthias Hetzenberger, Georg Moser, Florian Zuleger
2024	J	`jnl`	Deciding Boolean Separation Logic via Small Models (Technical Report). CoRR Tomás Dacík, Adam Rogalewicz, Tomás Vojnar, Florian Zuleger
2024	—	`conf`	Deciding Boolean Separation Logic via Small Models. TACAS (1) Tomás Dacík, Adam Rogalewicz, Tomás Vojnar, Florian Zuleger
2024	J	`jnl`	Effective MSO-Definability for Tree-width Bounded Models of an Inductive Separation Logic of Relations. CoRR Lucas Bueri, Radu Iosif, Florian Zuleger
2024	B	`conf`	Modeling Register Pairs in CompCert. IFM Alexander Loitzl, Florian Zuleger
2024	A*	`conf`	Probabilistic Synthesis and Verification for LTL on Finite Traces. KR Benjamin Aminof, Linus Cooper, Sasha Rubin, Moshe Y. Vardi, Florian Zuleger
2024	A*	`conf`	Proper Linear-time Specifications of Environment Behaviors in Nondeterministic Planning and Reactive Synthesis. KR Benjamin Aminof, Giuseppe De Giacomo, Sasha Rubin, Florian Zuleger
2024	J	`jnl`	Regular Grammars for Graph Sets of Tree-Width ≤. CoRR Marius Bozga, Radu Iosif, Florian Zuleger
2024	J	`jnl`	Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification. Formal Methods Syst. Des. Thomas Pani, Georg Weissenbacher, Florian Zuleger
2024	B	`conf`	Tree-Verifiable Graph Grammars. LPAR Mark Chimes, Radu Iosif, Florian Zuleger
2024	J	`jnl`	Tree-Verifiable Graph Grammars. CoRR Mark Chimes, Radu Iosif, Florian Zuleger
2023	J	`jnl`	A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions. ACM Trans. Comput. Log. Christoph Matheja, Jens Pagel, Florian Zuleger
2023	B	`conf`	A Formalization of Heisenbugs and Their Causes. SEFM Sarah Sallinger, Georg Weissenbacher, Florian Zuleger
2023	—	`conf`	Algorithmenerkennung und Programmreparatur mittels Dynamischer Programmanalyse. ABP Florian Zuleger
2023	J	`jnl`	Characterizations of Definable Context-Free Graphs. CoRR Radu Iosif, Florian Zuleger
2023	B	`conf`	Embedding Intuitionistic into Classical Logic. LPAR Alexander Pluska, Florian Zuleger
2023	B	`conf`	Expressiveness Results for an Inductive Logic of Separated Relations. CONCUR Radu Iosif, Florian Zuleger
2023	J	`jnl`	Expressiveness Results for an Inductive Logic of Separated Relations. CoRR Radu Iosif, Florian Zuleger
2023	J	`jnl`	Parameterized Model-checking of Discrete-Timed Networks and Symmetric-Broadcast Systems. CoRR Benjamin Aminof, Sasha Rubin, Francesco Spegni, Florian Zuleger
2023	J	`jnl`	Sound One-Phase Shape Analysis with Biabduction. CoRR Florian Sextl, Adam Rogalewicz, Tomás Vojnar, Florian Zuleger
2023	A*	`conf`	Stochastic Best-Effort Strategies for Borel Goals. LICS Benjamin Aminof, Giuseppe De Giacomo, Sasha Rubin, Florian Zuleger
2023	J	`jnl`	The Treewidth Boundedness Problem for an Inductive Separation Logic of Relations. CoRR Marius Bozga, Lucas Bueri, Radu Iosif, Florian Zuleger
2022	—	`conf`	Automated Expected Amortised Cost Analysis of Probabilistic Data Structures. CAV (2) Lorenz Leutgeb, Georg Moser, Florian Zuleger
2022	J	`jnl`	Automated Expected Amortised Cost Analysis of Probabilistic Data Structures. CoRR Lorenz Leutgeb, Georg Moser, Florian Zuleger
2022	A*	`conf`	Beyond Strong-Cyclic: Doing Your Best in Stochastic Environments. IJCAI Benjamin Aminof, Giuseppe De Giacomo, Sasha Rubin, Florian Zuleger
2022	J	`jnl`	Low-Level Bi-Abduction (Artifact). Dagstuhl Artifacts Ser. Lukás Holík, Petr Peringer, Adam Rogalewicz, Veronika Soková, Tomás Vojnar, Florian Zuleger
2022	A	`conf`	Low-Level Bi-Abduction. ECOOP Lukás Holík, Petr Peringer, Adam Rogalewicz, Veronika Soková, Tomás Vojnar, Florian Zuleger
2022	J	`jnl`	Low-Level Bi-Abduction. CoRR Lukás Holík, Petr Peringer, Adam Rogalewicz, Veronika Soková, Tomás Vojnar, Florian Zuleger
2022	J	`jnl`	On the Expressiveness of a Logic of Separated Relations. CoRR Radu Iosif, Florian Zuleger
2022	J	`jnl`	Strong-separation Logic. ACM Trans. Program. Lang. Syst. Jens Pagel, Florian Zuleger
2022	J	`jnl`	Type-based analysis of logarithmic amortised complexity. Math. Struct. Comput. Sci. Martin Hofmann, Lorenz Leutgeb, David Obwaller, Georg Moser, Florian Zuleger
2022	J	`jnl`	Verification of agent navigation in partially-known environments. Artif. Intell. Benjamin Aminof, Aniello Murano, Sasha Rubin, Florian Zuleger
2022	J	`jnl`	Verifying safety of synchronous fault-tolerant algorithms by bounded model checking. Int. J. Softw. Tools Technol. Transf. Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger
2021	—	`conf`	ATLAS: Automated Amortised Complexity Analysis of Self-adjusting Data Structures. CAV (2) Lorenz Leutgeb, Georg Moser, Florian Zuleger
2021	A	`conf`	Bounded Model Checking of Speculative Non-Interference. ICCAD Emmanuel Pescosta, Georg Weissenbacher, Florian Zuleger
2021	B	`conf`	Eliminating Message Counters in Synchronous Threshold Automata. VMCAI Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger
2021	J	`jnl`	Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. Formal Methods Syst. Des. Thomas Pani, Georg Weissenbacher, Florian Zuleger
2021	A	`conf`	Strong-Separation Logic. ESOP Jens Pagel, Florian Zuleger
2021	J	`jnl`	Type-Based Analysis of Logarithmic Amortised Complexity. CoRR Martin Hofmann, Lorenz Leutgeb, Georg Moser, David Obwaller, Florian Zuleger
2020	B	`conf`	Beyond Symbolic Heaps: Deciding Separation Logic With Inductive Definitions. LPAR Jens Katelaan, Florian Zuleger
2020	J	`jnl`	Complete Entailment Checking for Separation Logic with Inductive Definitions. CoRR Jens Pagel, Christoph Matheja, Florian Zuleger
2020	B	`conf`	Eliminating Message Counters in Threshold Automata. ATVA Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger
2020	A	`conf`	Multi-linear Strategy Extraction for QBF Expansion Proofs via Local Soundness. SAT Matthias Schlaipfer, Friedrich Slivovsky, Georg Weissenbacher, Florian Zuleger
2020	J	`jnl`	Strong-Separation Logic. CoRR Jens Pagel, Florian Zuleger
2020	B	`conf`	The Polynomial Complexity of Vector Addition Systems with States. FoSSaCS Florian Zuleger
2020	B	`conf`	Thread-modular Counter Abstraction for Parameterized Program Safety. FMCAD Thomas Pani, Georg Weissenbacher, Florian Zuleger
2019	—	`conf`	Effective Entailment Checking for Separation Logic with Inductive Definitions. TACAS (2) Jens Katelaan, Christoph Matheja, Florian Zuleger
2019	—	`conf`	SL-COMP: Competition of Solvers for Separation Logic. TACAS (3) Mihaela Sighireanu, Juan Antonio Navarro Pérez, 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, Tomás Vojnar, Constantin Enea, Ondrej Lengál, Chong Gao, Zhilin Wu
2019	J	`jnl`	The Polynomial Complexity of Vector Addition Systems with States. CoRR Florian Zuleger
2019	—	`conf`	Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking. TACAS (2) Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger
2018	A*	`conf`	Automated clustering and program repair for introductory programming assignments. PLDI Sumit Gulwani, Ivan Radicek, Florian Zuleger
2018	A*	`conf`	Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS. LICS Tomás Brázdil, Krishnendu Chatterjee, Antonín Kucera, Petr Novotný, Dominik Velan, Florian Zuleger
2018	J	`jnl`	Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS. CoRR Tomás Brázdil, Krishnendu Chatterjee, Antonín Kucera, Petr Novotný, Dominik Velan, Florian Zuleger
2018	B	`conf`	From Shapes to Amortized Complexity. VMCAI Tomás Fiedor, Lukás Holík, Adam Rogalewicz, Moritz Sinn, Tomás Vojnar, Florian Zuleger
2018	—	`conf`	Harrsh: A Tool for Unied Reasoning about Symbolic-Heap Separation Logic. LPAR (Workshop and Short Papers) Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger
2018	B	`conf`	Inductive Termination Proofs with Transition Invariants and Their Relationship to the Size-Change Abstraction. SAS Florian Zuleger
2018	J	`jnl`	Monadic refinements for relational cost analysis. Proc. ACM Program. Lang. Ivan Radicek, Gilles Barthe, Marco Gaboardi, Deepak Garg, Florian Zuleger
2018	B	`conf`	Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction. VMCAI Benjamin Aminof, Sasha Rubin, Ilina Stoilkovska, Josef Widder, Florian Zuleger
2018	B	`conf`	Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms. FMCAD Thomas Pani, Georg Weissenbacher, Florian Zuleger
2018	B	`conf`	Using Loop Bound Analysis For Invariant Generation. FMCAD Pavel Cadek, Clemens Danninger, Moritz Sinn, Florian Zuleger
2017	B	`conf`	Automata and Program Analysis. FCT Thomas Colcombet, Laure Daviaud, Florian Zuleger
2017	J	`jnl`	Complexity and Resource Bound Analysis of Imperative Programs Using Difference Constraints. J. Autom. Reason. Moritz Sinn, Florian Zuleger, Helmut Veith
2017	J	`jnl`	Empirical software metrics for benchmarking of verification tools. Formal Methods Syst. Des. Yulia Demyanova, Thomas Pani, Helmut Veith, Florian Zuleger
2017	A	`conf`	On the Automated Verification of Web Applications with Embedded SQL. ICDT Shachar Itzhaky, Tomer Kotek, Noam Rinetzky, Mooly Sagiv, Orr Tamir, Helmut Veith, Florian Zuleger
2017	J	`jnl`	Ranking Functions for Vector Addition Systems. CoRR Florian Zuleger
2017	J	`jnl`	Resource Bound Analysis (Dagstuhl Seminar 17291). Dagstuhl Reports Marco Gaboardi, Jan Hoffmann, Reinhard Wilhelm, Florian Zuleger
2017	—	`conf`	Systematic Predicate Abstraction Using Variable Roles. NFM Yulia Demyanova, Philipp Rümmer, Florian Zuleger
2017	A	`conf`	Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic. ESOP Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger
2016	C	`conf`	A simple and scalable static analysis for bound analysis and amortized complexity analysis. Software Engineering Moritz Sinn, Florian Zuleger, Helmut Veith
2016	J	`jnl`	Automated Clustering and Program Repair for Introductory Programming Assignments. CoRR Sumit Gulwani, Ivan Radicek, Florian Zuleger
2016	A	`conf`	Automatic Verification of Multi-Agent Systems in Parameterised Grid-Environments. AAMAS Benjamin Aminof, Aniello Murano, Sasha Rubin, Florian Zuleger
2016	C	`conf`	Empirical software metrics for benchmarking of verification tools. Software Engineering Yulia Demyanova, Thomas Pani, Helmut Veith, Florian Zuleger
2016	C	`conf`	Feedback generation for performance problems in introductory programming assignments. Software Engineering Florian Zuleger, Ivan Radicek, Sumit Gulwani
2016	J	`jnl`	Liveness of Parameterized Timed Networks. CoRR Benjamin Aminof, Sasha Rubin, Francesco Spegni, Florian Zuleger
2016	B	`conf`	Monadic Second Order Finite Satisfiability and Unbounded Tree-Width. CSL Tomer Kotek, Helmut Veith, Florian Zuleger
2016	J	`jnl`	On the automated verification of web applications with embedded SQL. CoRR Shachar Itzhaky, Tomer Kotek, Noam Rinetzky, Mooly Sagiv, Orr Tamir, Helmut Veith, Florian Zuleger
2016	A*	`conf`	Prompt Alternating-Time Epistemic Logics. KR Benjamin Aminof, Aniello Murano, Sasha Rubin, Florian Zuleger
2016	J	`jnl`	Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic. CoRR Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger
2015	Misc	`conf`	Asymptotically Precise Ranking Functions for Deterministic Size-Change Systems. CSR Florian Zuleger
2015	B	`conf`	Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs. FMCAD Moritz Sinn, Florian Zuleger, Helmut Veith
2015	J	`jnl`	Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs. CoRR Moritz Sinn, Florian Zuleger, Helmut Veith
2015	—	`conf`	Empirical Software Metrics for Benchmarking of Verification Tools. CAV (1) Yulia Demyanova, Thomas Pani, Helmut Veith, Florian Zuleger
2015	A*	`conf`	Extending ALCQIO with Trees. LICS Tomer Kotek, Mantas Simkus, Helmut Veith, Florian Zuleger
2015	—	`conf`	Liveness of Parameterized Timed Networks. ICALP (2) Benjamin Aminof, Sasha Rubin, Florian Zuleger, Francesco Spegni
2015	J	`jnl`	Loop Patterns in C Programs. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. Thomas Pani, Helmut Veith, Florian Zuleger
2015	J	`jnl`	Monadic second order finite satisfiability and unbounded tree-width. CoRR Tomer Kotek, Helmut Veith, Florian Zuleger
2015	B	`conf`	On the Expressive Power of Communication Primitives in Parameterised Systems. LPAR Benjamin Aminof, Sasha Rubin, Florian Zuleger
2015	B	`conf`	Verification of Asynchronous Mobile-Robots in Partially-Known Environments. PRIMA Sasha Rubin, Florian Zuleger, Aniello Murano, Benjamin Aminof
2014	A*	`conf`	A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis. CAV Moritz Sinn, Florian Zuleger, Helmut Veith
2014	J	`jnl`	A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis. CoRR Moritz Sinn, Florian Zuleger, Helmut Veith
2014	J	`jnl`	Extending ALCQIO with reachability. CoRR Tomer Kotek, Mantas Simkus, Helmut Veith, Florian Zuleger
2014	J	`jnl`	Feedback Generation for Performance Problems in Introductory Programming Assignments. CoRR Sumit Gulwani, Ivan Radicek, Florian Zuleger
2014	—	`conf`	Feedback generation for performance problems in introductory programming assignments. SIGSOFT FSE Sumit Gulwani, Ivan Radicek, Florian Zuleger
2014	B	`conf`	Shape and Content - A Database-Theoretic Perspective on the Analysis of Data Structures. IFM Diego Calvanese, Tomer Kotek, Mantas Simkus, Helmut Veith, Florian Zuleger
2014	—	`conf`	Shape and Content: Incorporating Domain Knowledge into Shape Analysis. Description Logics Diego Calvanese, Tomer Kotek, Mantas Simkus, Helmut Veith, Florian Zuleger
2014	—	`conf`	Size-Change Abstraction and Max-Plus Automata. MFCS (1) Thomas Colcombet, Laure Daviaud, Florian Zuleger
2014	—	`conf`	Towards a Description Logic for Program Analysis: Extending ALCQIO with Reachability. Description Logics Tomer Kotek, Mantas Simkus, Helmut Veith, Florian Zuleger
2013	J	`jnl`	On the Concept of Variable Roles and its Use in Software Analysis CoRR Yulia Demyanova, Helmut Veith, Florian Zuleger
2013	B	`conf`	On the concept of variable roles and its use in software analysis. FMCAD Yulia Demyanova, Helmut Veith, Florian Zuleger
2013	A	`conf`	Ramsey vs. Lexicographic Termination Proving. TACAS Byron Cook, Abigail See, Florian Zuleger
2013	J	`jnl`	Shape and Content: Incorporating Domain Knowledge into Shape Analysis. CoRR Diego Calvanese, Tomer Kotek, Mantas Simkus, Helmut Veith, Florian Zuleger
2012	J	`jnl`	Bound Analysis of Imperative Programs with the Size-change Abstraction (extended version) CoRR Florian Zuleger, Sumit Gulwani, Moritz Sinn, Helmut Veith
2011	B	`conf`	Bound Analysis of Imperative Programs with the Size-Change Abstraction. SAS Florian Zuleger, Sumit Gulwani, Moritz Sinn, Helmut Veith
2010	—	`conf`	LOOPUS - A Tool for Computing Loop Bounds for C Programs. WING@ETAPS/IJCAR Moritz Sinn, Florian Zuleger
2010	A*	`conf`	The reachability-bound problem. PLDI Sumit Gulwani, Florian Zuleger
2009	B	`conf`	An Abstract Interpretation-Based Framework for Control Flow Reconstruction from Binaries. VMCAI Johannes Kinder, Florian Zuleger, Helmut Veith