TU Wien Informatics

Overview Professors Scientific Staff Administrative Staff Student Staff External Lecturers By Responsibilities By Committee By Name
Related
Guest Professors Honoraries Alumni (LinkedIn) #5qw

Florian Zuleger

Associate Prof. Dipl.-Math. Dr.techn.

Research Focus

  • Logic and Computation: 100%

Research Areas

  • Verification, Program Analysis, Computational Logic, Formal Methods, Automata Theory, logic in computer science
Florian Zuleger

About

automated methods for termination and resource-bound analysis,verification of programs with dynamic data structures and embedded database-queries, parameterized verification, automated feedback generation for introductory programming assignments.

Roles

Contact

2024W

2025S

 

2025

2024

  • Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification / Pani, T., Weissenbacher, G., & Zuleger, F. (2024). Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification. Formal Methods in System Design, 64(1–3), 108–145. https://doi.org/10.1007/s10703-023-00439-6
  • Modeling Register Pairs in CompCert / Loitzl, A., & Zuleger, F. (2024). Modeling Register Pairs in CompCert. In N. Kosmatov & L. Kovács (Eds.), Integrated Formal Methods : 19th International Conference, IFM 2024 Manchester, UK, November 13–15, 2024 Proceedings (pp. 128–147). Springer. https://doi.org/10.1007/978-3-031-76554-4_8
  • Proper Linear-time Specifications of Environment Behaviors in Nondeterministic Planning and Reactive Synthesis / Aminof, B., De Giacomo, G., Rubin, S., & Zuleger, F. (2024). Proper Linear-time Specifications of Environment Behaviors in Nondeterministic Planning and Reactive Synthesis. In Proceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning (pp. 38–48). IJCAI Organization. https://doi.org/10.24963/kr.2024/4
  • Tree-Verifiable Graph Grammars / Chimes, M. J., Iosif, R., & Zuleger, F. (2024). Tree-Verifiable Graph Grammars. In Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning (pp. 165–180). https://doi.org/10.29007/8l13
  • Deciding Boolean Separation Logic via Small Models / Dacík, T., Rogalewicz, A., Vojnar, T., & Zuleger, F. (2024). Deciding Boolean Separation Logic via Small Models. In Tools and Algorithms for the Construction and Analysis of Systems : 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6–11, 2024, Proceedings, Part I (pp. 188–206). springer. https://doi.org/10.1007/978-3-031-57246-3_11
  • Probabilistic Synthesis and Verification for LTL on Finite Traces / Aminof, B., Cooper, L., Rubin, S., Vardi, M. Y., & Zuleger, F. (2024). Probabilistic Synthesis and Verification for LTL on Finite Traces. In P. Marquis, M. Ortiz, & M. Pagnucco (Eds.), Proceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning (pp. 27–37). IJCAI Organization. https://doi.org/10.24963/kr.2024/3

2023

2022

  • Strong-separation Logic (Extended Version) / Pagel, J., & Zuleger, F. (2022). Strong-separation Logic (Extended Version). ACM Letters on Programming Languages and Systems, 44(3), 1–40. https://doi.org/10.1145/3498847
  • Automated Expected Amortised Cost Analysis of Probabilistic Data Structures / Leutgeb, L., Moser, G., & Zuleger, F. (2022). Automated Expected Amortised Cost Analysis of Probabilistic Data Structures. In Computer Aided Verification - 34th International Conference, CAV 2022 (pp. 70–91). https://doi.org/10.1007/978-3-031-13188-2_4
  • Verification of agent navigation in partially-known environments / Aminof, B., Murano, A., Rubin, S., & Zuleger, F. (2022). Verification of agent navigation in partially-known environments. Artificial Intelligence, 308, Article 103724. https://doi.org/10.1016/j.artint.2022.103724
  • Beyond Strong-Cyclic: Doing Your Best in Stochastic Environments / Aminof, B., De Giacomo, G., Rubin, S., & Zuleger, F. (2022). Beyond Strong-Cyclic: Doing Your Best in Stochastic Environments. In Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence (pp. 2525–2531). https://doi.org/10.24963/ijcai.2022/350
  • Low-Level Bi-Abduction / Holík, L., Peringer, P., Rogalewicz, A., Šoková, V., Vojnar, T., & Zuleger, F. (2022). Low-Level Bi-Abduction. In 36th European Conference on Object-Oriented Programming (ECOOP 2022) (pp. 1–30). Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.ECOOP.2022.19
    Download: PDF (1.2 MB)
  • Verifying safety of synchronous fault-tolerant algorithms by bounded model checking / Stoilkovska, I., Konnov, I., Widder, J., & Zuleger, F. (2022). Verifying safety of synchronous fault-tolerant algorithms by bounded model checking. International Journal on Software Tools for Technology Transfer, 24(1), 33–48. https://doi.org/10.1007/s10009-021-00637-9
  • ATLAS: Automated Amortised Complexity Analysis of Self-adjusting Data Structures / Leutgeb, L., Moser, G., & Zuleger, F. (2022). ATLAS: Automated Amortised Complexity Analysis of Self-adjusting Data Structures. In Computer Aided Verification (pp. 99–122). https://doi.org/10.1007/978-3-030-81688-9_5
  • Strong-separation Logic / Pagel, J., & Zuleger, F. (2022). Strong-separation Logic. In ESOP 2021: Programming Languages and Systems (pp. 664–692). Springer. https://doi.org/10.1007/978-3-030-72019-3_24

2021

  • Bounded Model Checking of Speculative Non-Interference / Pescosta, E., Weissenbacher, G., & Zuleger, F. (2021). Bounded Model Checking of Speculative Non-Interference. In 2021 IEEE/ACM International Conference On Computer Aided Design (ICCAD). 2021 IEEE/ACM International Conference On Computer Aided Design (ICCAD), München, Germany. IEEE. https://doi.org/10.1109/iccad51958.2021.9643462
  • Eliminating Message Counters in Synchronous Threshold Automata / Stoilkovska, I., Konnov, I., Widder, J., & Zuleger, F. (2021). Eliminating Message Counters in Synchronous Threshold Automata. In VMCAI 2021: Verification, Model Checking, and Abstract Interpretation (pp. 196–218). Springer LNCS. https://doi.org/10.1007/978-3-030-67067-2_10
  • Rely-guarantee bound analysis of parameterized concurrent shared-memory programs / Pani, T., Weissenbacher, G., & Zuleger, F. (2021). Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. Formal Methods in System Design, 57(2), 270–302. https://doi.org/10.1007/s10703-021-00370-8

2020

  • Eliminating Message Counters in Threshold Automata / Stoilkovska, I., Konnov, I., Widder, J., & Zuleger, F. (2020). Eliminating Message Counters in Threshold Automata. In Automated Technology for Verification and Analysis. 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings (pp. 192–212). Springer. https://doi.org/10.34726/423
    Download: PDF (408 KB)
  • Thread-modular Counter Abstraction for Parameterized Program Safety / Pani, T., Weissenbacher, G., & Zuleger, F. (2020). Thread-modular Counter Abstraction for Parameterized Program Safety. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 (pp. 67–76). TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_13
    Download: Published version (434 KB)
  • The Polynomial Complexity of Vector Addition Systems with States / Zuleger, F. (2020). The Polynomial Complexity of Vector Addition Systems with States. In Foundations of Software Science and Computation Structures 23rd International Conference, FOSSACS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020, Proceedings (pp. 622–641). Springer LNCS. https://doi.org/10.1007/978-3-030-45231-5_32
  • Thread-modular Counter Abstraction for Parameterized Program Safety / Pani, T., Weissenbacher, G., & Zuleger, F. (2020). Thread-modular Counter Abstraction for Parameterized Program Safety. In Formal Methods in Computer-Aided Design (pp. 67–76). TU Wien Academic Press / IEEE. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_13
  • Multi-linear Strategy Extraction for QBF Expansion Proofs via Local Soundness / Schlaipfer, M., Slivovsky, F., Weissenbacher, G., & Zuleger, F. (2020). Multi-linear Strategy Extraction for QBF Expansion Proofs via Local Soundness. In Theory and Applications of Satisfiability Testing – SAT 2020 (pp. 429–446). LNCS. https://doi.org/10.1007/978-3-030-51825-7_30
  • Beyond Symbolic Heaps: Deciding Separation Logic With Inductive Definitions / Pagel, J., & Zuleger, F. (2020). Beyond Symbolic Heaps: Deciding Separation Logic With Inductive Definitions. In EPiC Series in Computing. EasyChair EPiC Series in Computing. https://doi.org/10.29007/vkmj

2019

2018

  • Automated clustering and program repair for introductory programming assignments / Radicek, I., Gulwani, S., & Zuleger, F. (2018). Automated clustering and program repair for introductory programming assignments. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation. Conference on Programming Language Design and Implementation (PLDI), Ottawa, Canada. ACM. https://doi.org/10.1145/3192366.3192387
  • Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms / Pani, T., Weissenbacher, G., & Zuleger, F. (2018). Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms. In 2018 Formal Methods in Computer Aided Design (FMCAD). International Conference on Formal Methods in Computer-Aided Design (FMCAD), Portland, United States of America (the). FMCAD Inc. https://doi.org/10.23919/fmcad.2018.8603020
  • Using Loop Bound Analysis For Invariant Generation / Cadek, P., Danninger, C., Sinn, M., & Zuleger, F. (2018). Using Loop Bound Analysis For Invariant Generation. In 2018 Formal Methods in Computer Aided Design (FMCAD). International Conference on Formal Methods in Computer-Aided Design (FMCAD), Portland, United States of America (the). FMCAD Inc. https://doi.org/10.23919/fmcad.2018.8603005
  • Monadic refinements for relational cost analysis / Radiček, I., Barthe, G., Gaboardi, M., Garg, D., & Zuleger, F. (2018). Monadic refinements for relational cost analysis. In Proceedings of the ACM on Programming Languages (pp. 1–32). ACM Digital Library. https://doi.org/10.1145/3158124
  • Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS / Brázdil, T., Chatterjee, K., Kučera, A., Novotný, P., Velan, D., & Zuleger, F. (2018). Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. Symposium on Logic in Computer Science (LICS), Edinburgh, United Kingdom of Great Britain and Northern Ireland (the). ACM. https://doi.org/10.1145/3209108.3209191
  • Inductive Termination Proofs with Transition Invariants and Their Relationship to the Size-Change Abstraction / Zuleger, F. (2018). Inductive Termination Proofs with Transition Invariants and Their Relationship to the Size-Change Abstraction. In Static Analysis (pp. 423–444). Springer. https://doi.org/10.1007/978-3-319-99725-4_25
  • Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction / Aminof, B., Rubin, S., Stoilkovska, I., Widder, J., & Zuleger, F. (2018). Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction. In I. Dillig & J. Palsberg (Eds.), Verification, Model Checking, and Abstract Interpretation : 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings. Cham. https://doi.org/10.1007/978-3-319-73721-8_1
    Download: PDF (538 KB)
  • From Shapes to Amortized Complexity / Fiedor, T., Holík, L., Rogalewicz, A., Sinn, M., Vojnar, T., & Zuleger, F. (2018). From Shapes to Amortized Complexity. In I. Dillig & J. Palsberg (Eds.), Verification, Model Checking, and Abstract Interpretation : 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings. Los Angeles. https://doi.org/10.1007/978-3-319-73721-8_10
    Download: PDF (426 KB)

2017

  • Automata and Program Analysis / Daviaud, L., Colcombet, T., & Zuleger, F. (2017). Automata and Program Analysis. In Fundamentals of Computation Theory - 21st International Symposium, FCT 2017 (pp. 3–10). http://hdl.handle.net/20.500.12708/57151
  • Systematic Predicate Abstraction using Variable Roles / Demyanova, Y., Rümmer, P., & Zuleger, F. (2017). Systematic Predicate Abstraction using Variable Roles. In C. Barrett, M. Davies, & T. Kahsai (Eds.), NASA Formal Methods : 9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16-18, 2017, Proceedings. Springer Cham. https://doi.org/10.1007/978-3-319-57288-8_18
    Download: PDF (369 KB)
  • Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic / Jansen, C., Pagel, J., Matheja, C., Noll, T., & Zuleger, F. (2017). Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic. In H. Yang (Ed.), Programming Languages and Systems : 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017, Proceedings. Springer Berlin. https://doi.org/10.1007/978-3-662-54434-1_23
    Download: PDF (571 KB)
  • Complexity and Resource Bound Analysis of Imperative Programs Using Difference Constraints / Sinn, M., Zuleger, F., & Veith, H. (2017). Complexity and Resource Bound Analysis of Imperative Programs Using Difference Constraints. Journal of Automated Reasoning, 59(1), 3–45. https://doi.org/10.1007/s10817-016-9402-4
    Download: PDF (1.71 MB)
    Project: Automated Bound Analysis (2013–2016)
  • Empirical software metrics for benchmarking of verification tools / Demyanova, Y., Pani, T., Veith, H., & Zuleger, F. (2017). Empirical software metrics for benchmarking of verification tools. Formal Methods in System Design, 50(2–3), 289–316. https://doi.org/10.1007/s10703-016-0264-5
  • On the Automated Verification of Web Applications with Embedded SQL / Shachar, I., Kotek, T., Rinetzky, N., Sagiv, M., Tamir, O., Veith, H., & Zuleger, F. (2017). On the Automated Verification of Web Applications with Embedded SQL. In 20th International Conference on Database Theory, ICDT 2017 (pp. 1–18). http://hdl.handle.net/20.500.12708/57152

2016

2015

  • On the expressive power of communication primitives in parameterised systems / Aminof, B., Rubin, S., & Zuleger, F. (2015). On the expressive power of communication primitives in parameterised systems. In M. Davis, A. Fehnker, A. McIver, & A. Voronkov (Eds.), Logic for Programming, Artificial Intelligence, and Reasoning : 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings (pp. 313–328). Springer. https://doi.org/10.1007/978-3-662-48899-7_22
    Download: PDF (438 KB)
  • Verification of Asynchronous Mobile-Robots in Partially-Known Environments / Aminof, B., Murano, A., Rubin, S., & Zuleger, F. (2015). Verification of Asynchronous Mobile-Robots in Partially-Known Environments. In Q. Chen, P. Torroni, S. Villata, J. Hsu, & A. Omicini (Eds.), PRIMA 2015: Principles and Practice of Multi-Agent Systems : 18th International Conference, Bertinoro, Italy, October 26-30, 2015, Proceedings (FP7 EU: 600958-SHERPA). Cham. https://doi.org/10.1007/978-3-319-25524-8_12
    Download: PDF (412 KB)
  • Loop Patterns in C Programs / Pani, T., Veith, H., & Zuleger, F. (2015). Loop Patterns in C Programs. ECEASST, 72. http://hdl.handle.net/20.500.12708/151928
  • Asymptotically Precise Ranking Functions for Deterministic Size-Change Systems / Zuleger, F. (2015). Asymptotically Precise Ranking Functions for Deterministic Size-Change Systems. In Computer Science -- Theory and Applications 10th International Computer Science Symposium in Russia, CSR 2015, Listvyanka, Russia, July 13-17, 2015, Proceedings (pp. 426–442). Springer. https://doi.org/10.1007/978-3-319-20297-6_27
  • Liveness of Parameterized Timed Networks / Aminof, B., Rubin, S., Spegni, F., & Zuleger, F. (2015). Liveness of Parameterized Timed Networks. In Automata, Languages, and Programming (pp. 375–387). Springer. https://doi.org/10.1007/978-3-662-47666-6_30
  • Empirical Software Metrics for Benchmarking of Verification Tools / Demyanova, Y., Pani, T., Veith, H., & Zuleger, F. (2015). Empirical Software Metrics for Benchmarking of Verification Tools. In Computer Aided Verification (pp. 561–579). Springer. https://doi.org/10.1007/978-3-319-21690-4_39
  • Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs / Sinn, M., Veith, H., & Zuleger, F. (2015). Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs. In FMCAD (pp. 144–151). http://hdl.handle.net/20.500.12708/56391
  • Extending ALCQIO with Trees / Kotek, T., imkus, M., Veith, H., & Zuleger, F. (2015). Extending ALCQIO with Trees. In 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science. 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2015), Kyoto, Japan, Austria. IEEE. https://doi.org/10.1109/lics.2015.54
    Projects: Automated Bound Analysis (2013–2016) / FAIR (2013–2018) / PROSEED (2011–2015) / SEE (2012–2016)

2014

2013

  • On the concept of variable roles and its use in software analysis / Demyanova, Y., Veith, H., & Zuleger, F. (2013). On the concept of variable roles and its use in software analysis. In FMCAD (pp. 226–230). IEEE. http://hdl.handle.net/20.500.12708/54835
  • Ramsey vs. Lexicographic Termination Proving / Cook, B., See, A., & Zuleger, F. (2013). Ramsey vs. Lexicographic Termination Proving. In Tools and Algorithms for the Construction and Analysis of Systems (pp. 47–61). Lecture Notes in Computer Science. Springer Verlag. https://doi.org/10.1007/978-3-642-36742-7_4

2011

2010

  • The reachability-bound problem / Gulwani, S., & Zuleger, F. (2010). The reachability-bound problem. In B. G. Zorn & A. Aiken (Eds.), Proceedings of the 2010 ACM SIGPLAN conference on Programming language design and implementation - PLDI ’10. PLDI’10 Proceedings of teh ACM SIGPLAN conference on Programming language design and implementation. https://doi.org/10.1145/1806596.1806630

 

  • Verication of Asynchronous Mobile-Robots in Partially-Known Environments
    2015 / Best Paper Award / Italy (South Tyrol)

Soon, this page will include additional information such as reference projects, activities as journal reviewer and editor, memberships in councils and committees, and other research activities.

Until then, please visit Florian Zuleger’s research profile in TISS .