2023W

• Bachelor Thesis / 184.695 / PR
• Doctoral & Master Students Seminar / 181.224 / SE
• Formal Methods in Computer Science / 185.A93 / UE
• Formal Methods in Computer Science / 185.291 / VU
• Introduction to Logical Methods in Computer Science / 184.766 / VO
• Program Analysis / 184.703 / VU
• Project in Computer Science 1 / 192.021 / PR
• Project in Computer Science 2 / 192.022 / PR
• Research Seminar LogiCS / 184.767 / SE
• Scientific Research and Writing / 193.052 / SE
• Seminar for Master Students in Logic and Computation / 180.773 / SE

2024S

• Bachelor Thesis / 184.695 / PR
• Doctoral & Master Students Seminar / 181.224 / SE
• Introduction to Logical Methods in Computer Science / 184.766 / VO
• Project in Computer Science 1 / 192.021 / PR
• Project in Computer Science 2 / 192.022 / PR
• Research Seminar LogiCS / 184.767 / SE
• Semantics of Programming Languages / 184.749 / VU
• Seminar for Master Students in Logic and Computation / 180.773 / SE
• Seminar Formal Methods / 181.221 / SE

• Automated Sublinear Amortised Resource Analysis of Data Structures
  2023 – 2027 / Austrian Science Fund (FWF)
• Automated Cost Analysis of Data Structures
  2023 – 2024 / Amazon Research Awards
• Automated Program Analysis for Bounds on Resource Consumption
  2013 – 2016 / Vienna Science and Technology Fund (WWTF)
  Publication: 56097
• Automatic Derivation of Loop Bounds for Worst Case Execution Time Analysis
  2009 – 2015 / MICROSOFT RESEARCH LIMITED

2023

• A Formalization of Heisenbugs and Their Causes / Sallinger, S., Weissenbacher, G., & Zuleger, F. (2023). A Formalization of Heisenbugs and Their Causes. In C. Ferreira & T. A. C. Willemse (Eds.), Software Engineering and Formal Methods : 21st International Conference, SEFM 2023, Eindhoven, The Netherlands, November 6-10, 2023, Proceedings (pp. 282–300). Springer. https://doi.org/10.34726/5381
  Project: ARTIST (2021–2026)
• Embedding Intuitionistic into Classical Logic / Pluska, A., & Zuleger, F. (2023). Embedding Intuitionistic into Classical Logic. In R. Piskac & A. Voronkov (Eds.), Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (pp. 329–349). https://doi.org/10.29007/b294
• Expressiveness Results for an Inductive Logic of Separated Relations / Iosif, R., & Zuleger, F. (2023). Expressiveness Results for an Inductive Logic of Separated Relations. In 34th International Conference on Concurrency Theory (CONCUR 2023). 34th International Conference on Concurrency Theory, CONCUR 2023, Antwerp, Belgium. Schloss-Dagstuhl - Leibniz Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2023.20
  Download: PDF (918 KB)
• Stochastic Best-Effort Strategies for Borel Goals / Aminof, B., De Giacomo, G., Rubin, S., & Zuleger, F. (2023). Stochastic Best-Effort Strategies for Borel Goals. In 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Boston, MA, United States of America (the). IEEE. https://doi.org/10.1109/LICS56636.2023.10175747
• A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions / Matheja, C., Pagel, J., & Zuleger, F. (2023). A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions. ACM Transactions on Computational Logic, 24(1), 1–76. https://doi.org/10.1145/3534927

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
• 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
• 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
• 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

• 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
• 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

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)
• 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
• The Polynomial Complexity of Vector Addition Systems with States / Zuleger, F. (2020). The Polynomial Complexity of Vector Addition Systems with States. In Lecture Notes in Computer Science (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

2019

• Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking / Stoilkovska, I., Konnov, I., Widder, J., & Zuleger, F. (2019). Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (pp. 357–374). Springer. http://hdl.handle.net/20.500.12708/56804
• SL-COMP: Competition of Solvers for Separation Logic / Sighireanu, M., Pagel, J., Matheja, C., Noll, T., & Zuleger, F. (2019). SL-COMP: Competition of Solvers for Separation Logic. In 25th International Conference, TACAS 2019 (pp. 116–132). Springer. http://hdl.handle.net/20.500.12708/57483
• Effective Entailment Checking for Separation Logic with Inductive Definitions / Pagel, J., Matheja, C., & Zuleger, F. (2019). Effective Entailment Checking for Separation Logic with Inductive Definitions. In 25th International Conference, TACAS 2019 (pp. 319–336). Springer. http://hdl.handle.net/20.500.12708/57482

2018

• 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
• 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)
• 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

• Monadic Second Order Finite Satisfiability and Unbounded Tree-Width / Kotek, T., Veith, H., & Zuleger, F. (2016). Monadic Second Order Finite Satisfiability and Unbounded Tree-Width. In CSL (pp. 1–20). http://hdl.handle.net/20.500.12708/56860
• Automatic Verification of Multi-Agent Systems in Parameterised Grid-Environments / Aminof, B., Murano, A., Rubin, S., & Zuleger, F. (2016). Automatic Verification of Multi-Agent Systems in Parameterised Grid-Environments. In AAMAS (pp. 1190–1199). http://hdl.handle.net/20.500.12708/56859
• Prompt Alternating-Time Epistemic Logics / Aminof, B., Murano, A., Rubin, S., & Zuleger, F. (2016). Prompt Alternating-Time Epistemic Logics. In KR (pp. 258–267). http://hdl.handle.net/20.500.12708/56836

2015

• 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
• 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
• 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
• Asymptotically Precise Ranking Functions for Deterministic Size-Change Systems / Zuleger, F. (2015). Asymptotically Precise Ranking Functions for Deterministic Size-Change Systems. In Lecture Notes in Computer Science (pp. 426–442). Springer. https://doi.org/10.1007/978-3-319-20297-6_27
• 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

• Towards a Description Logic for Program Analysis: Extending ALCQIO with Reachability / Kotek, T., Simkus, M., Veith, H., & Zuleger, F. (2014). Towards a Description Logic for Program Analysis: Extending ALCQIO with Reachability. In International Workshop on Description Logics (p. 4). http://hdl.handle.net/20.500.12708/55329
• Shape and Content: Incorporating Domain Knowledge into Shape Analysis / Calvanese, D., Kotek, T., Simkus, M., Veith, H., & Zuleger, F. (2014). Shape and Content: Incorporating Domain Knowledge into Shape Analysis. In International Workshop on Description Logics (p. 4). http://hdl.handle.net/20.500.12708/55330
• Shape and Content - A Database-Theoretic Perspective on the Analysis of Data Structures / Calvanese, D., Kotek, T., Šimkus, M., Veith, H., & Zuleger, F. (2014). Shape and Content - A Database-Theoretic Perspective on the Analysis of Data Structures. In E. Albert & E. Sekerinski (Eds.), Integrated Formal Methods (pp. 3–17). Springer / LNCS. https://doi.org/10.1007/978-3-319-10181-1_1
• Size-Change Abstraction and Max-Plus Automata / Colcombet, T., Daviaud, L., & Zuleger, F. (2014). Size-Change Abstraction and Max-Plus Automata. In Mathematical Foundations of Computer Science 2014 (pp. 208–219). Springer / LNCS. https://doi.org/10.1007/978-3-662-44522-8_18
• Feedback generation for performance problems in introductory programming assignments / Gulwani, S., Radiček, I., & Zuleger, F. (2014). Feedback generation for performance problems in introductory programming assignments. In Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering. ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE), Hong Kong, China, Non-EU. ACM New York, NY, USA. https://doi.org/10.1145/2635868.2635912
• A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis / Sinn, M., Zuleger, F., & Veith, H. (2014). A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis. In Computer Aided Verification (pp. 745–761). Springer / LNCS. https://doi.org/10.1007/978-3-319-08867-9_50

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

• Termination and Bound Analysis of Imperative Programs / Zuleger, F. (2011). Termination and Bound Analysis of Imperative Programs. Workshop on Logic and Computer Science, Vienna, Austria. http://hdl.handle.net/20.500.12708/85314
• Bound Analysis of Imperative Programs with the Size-change Abstraction / Zuleger, F. (2011). Bound Analysis of Imperative Programs with the Size-change Abstraction. Software Systems Group Seminar, NICTA, Australien, Non-EU. http://hdl.handle.net/20.500.12708/85313
• Bound Analysis of Imperative Programs with the Size-change Abstraction / Zuleger, F. (2011). Bound Analysis of Imperative Programs with the Size-change Abstraction. Austrian Society for Rigorous Systems Engineering (ARiSE) workshop together with PUMA workshop, Traunkirchen, Austria, Austria. http://hdl.handle.net/20.500.12708/85312
• Resource Bound Analysis of Imperative Programs / Zuleger, F. (2011). Resource Bound Analysis of Imperative Programs. RiSE Seminar, Klosterneuburg, Austria. http://hdl.handle.net/20.500.12708/85142
• Bound Analysis of Imperative Programs with the Size-change Abstraction / Zuleger, F. (2011). Bound Analysis of Imperative Programs with the Size-change Abstraction. Microsoft Research Lecture, Microsoft Research Cambridge, UK, EU. http://hdl.handle.net/20.500.12708/84682
• Bound Analysis of Imperative Programs with the Size-change Abstraction / Zuleger, F. (2011). Bound Analysis of Imperative Programs with the Size-change Abstraction. Theory Seminar, Queen Mary University, UK, EU. http://hdl.handle.net/20.500.12708/84681
• Bound Analysis of Imperative Programs with the Size-Change Abstraction / Zuleger, F., Sinn, M., Gulwani, S., & Veith, H. (2011). Bound Analysis of Imperative Programs with the Size-Change Abstraction. In E. Yahav (Ed.), Static Analysis (pp. 280–297). Springer. https://doi.org/10.1007/978-3-642-23702-7_22
  Projects: PROSEED (2011–2015) / Rise-TOOLS (2011–2019)

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

• Enhancing abstraction and symbolic execution for shape analysis of C-programs operating on linked lists / Kaindlstorfer, D. (2023). Enhancing abstraction and symbolic execution for shape analysis of C-programs operating on linked lists [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2023.109623
  Download: PDF (591 KB)
• Modeling and verification of synchronous fault-tolerant distributed algorithms / Stoilkovska, I. (2021). Modeling and verification of synchronous fault-tolerant distributed algorithms [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2021.90331
  Download: PDF (2.67 MB)
• Thread-modular verification of parameterized programs / Pani, T. (2021). Thread-modular verification of parameterized programs [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2022.100625
  Download: PDF (1.57 MB)
• ATLAS: Automated amortised complexity analysis of self-adjusting data structures / Leutgeb, L. (2021). ATLAS: Automated amortised complexity analysis of self-adjusting data structures [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2021.91302
  Download: PDF (931 KB)
• Decision procedures for separation logic: beyond symbolic heaps / Pagel, J. (2020). Decision procedures for separation logic: beyond symbolic heaps [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2020.85941
  Download: PDF (2.17 MB)
• SpecBMC : bounded model checker for speculative non-interference / Pescosta, E. (2020). SpecBMC : bounded model checker for speculative non-interference [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2020.76820
  Download: PDF (1.89 MB)
• Automated feedback generation in introductory programming education : a dynamic program analysis approach / Radiček, I. (2020). Automated feedback generation in introductory programming education : a dynamic program analysis approach [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2020.78440
  Download: PDF (1.36 MB)
• Rendezvous-multiple broadcast networks / Hafner, J. (2018). Rendezvous-multiple broadcast networks [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2018.32122
  Download: PDF (1.28 MB)
• Interactive lecture notes : a computer-aided education system for mastery learning via flipped classrooms / Geiger, S. S. (2018). Interactive lecture notes : a computer-aided education system for mastery learning via flipped classrooms [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2018.58222
  Download: PDF (2.62 MB)
• Systematic study of variable roles and their use in software verification / Demyanova, Y. (2018). Systematic study of variable roles and their use in software verification [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2018.54905
  Download: PDF (2.2 MB)
• Resource Bound-Analyse von Lisp-Programmen / Danninger, C. F. (2016). Resource Bound-Analyse von Lisp-Programmen [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2016.40480
  Download: PDF (511 KB)
• Automated complexity analysis for imperative programs / Sinn, M. (2016). Automated complexity analysis for imperative programs [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2016.40011
  Download: PDF (1.49 MB)
• Bounds for variables and loops: better together / Souczek, F. (2014). Bounds for variables and loops: better together [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2014.25323
  Download: PDF (843 KB)
• Loop patterns in C programs / Pani, T. (2013). Loop patterns in C programs [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2013.23344
  Download: PDF (710 KB)

• 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 .