TU Wien Informatics

20 Years

Florian Zuleger

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

Research Focus

Research Areas

  • Verification, Program Analysis, 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.

Role

2023

2022

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, Deutschland, EU. 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

2019

2018

  • 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 Verification, Model Checking, and Abstract Interpretation - 19th International , VMCAI 2018, Los Angeles, CA, USA, January 7-9, Proceedings ; Dillig, Isil; Palsberg, Jens. Los Angeles. https://doi.org/10.1007/978-3-319-73721-8_10
    Download: PDF (426 KB)
  • 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 Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings ; Dillig, Isil; Palsberg, Jens. Cham. https://doi.org/10.1007/978-3-319-73721-8_1
    Download: PDF (538 KB)
  • 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, OR, USA, Non-EU. FMCAD Inc. https://doi.org/10.23919/fmcad.2018.8603005
  • 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
  • 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, EU. ACM. https://doi.org/10.1145/3209108.3209191
  • 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
  • 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, OR, USA, Non-EU. FMCAD Inc. https://doi.org/10.23919/fmcad.2018.8603020
  • 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, Non-EU. ACM. https://doi.org/10.1145/3192366.3192387

2017

  • 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)
  • Systematic Predicate Abstraction using Variable Roles / Demyanova, Y., Rümmer, P., & Zuleger, F. (2017). Systematic Predicate Abstraction using Variable Roles. In NASA Formal Methods - 9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16-18, 2017, Proceedings ; Barrett, Clark; Davies, Misty; Kahsai, Temesghen. Cham. https://doi.org/10.1007/978-3-319-57288-8_18
    Download: PDF (369 KB)
  • 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
  • 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

2016

2015

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

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 .