Florian Zuleger
Associate Prof. Dipl.-Math. Dr.techn.
Research Focus
- Logic and Computation: 100%
Research Areas
- Verification, Program Analysis, Formal Methods, Automata Theory, logic in computer science
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
-
Associate Professor
Formal Methods in Systems Engineering, E192-04
Courses
2022W
- 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 / 184.692 / PR
- Project in Computer Science 2 / 184.693 / 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
- Seminar Formal Methods / 181.221 / SE
2023S
- Bachelor Thesis / 184.695 / PR
- Doctoral & Master Students Seminar / 181.224 / SE
- Formal Methods in Computer Science / 185.291 / VU
- Introduction to Logical Methods in Computer Science / 184.766 / VO
- Project in Computer Science 1 / 184.692 / PR
- Project in Computer Science 2 / 184.693 / PR
- Research Seminar LogiCS / 184.767 / SE
- Scientific Research and Writing / 193.052 / SE
- Semantics of Programming Languages / 184.749 / VU
- Seminar Formal Methods / 181.221 / SE
Projects
-
Automated Program Analysis for Bounds on Resource Consumption
2013 – 2016 / Vienna Science and Technology Fund (WWTF) -
Automatic Derivation of Loop Bounds for Worst Case Execution Time Analysis
2009 – 2015 / MICROSOFT RESEARCH LIMITED
Publications
Note: Due to the rollout of TU Wien’s new publication database, the list below may be slightly outdated. Once APIs for the new database have been released, everything will be up to date again.
2022
- ATLAS: Automated Amortised Complexity Analysis of Self-adjusting Data Structures / L. Leutgeb, G. Moser, F. Zuleger / Talk: International Conference on Computer Aided Verification (CAV), virtuell; 2022-07-20 - 2022-07-23; in: "CAV 2021: Computer Aided Verification", (2022), 99 - 122
2021
- Bounded Model Checking of Speculative Non-Interference / E. Pescosta, G. Weissenbacher, F. Zuleger / Talk: 2021 IEEE/ACM International Conference On Computer Aided Design (ICCAD), München, Deutschland; 2021-11-01 - 2021-11-04; in: "2021 IEEE/ACM International Conference On Computer Aided Design (ICCAD)", IEEE, (2021), ISBN: 978-1-6654-4507-8; 1 - 9
- Strong-Separation Logic / J. Pagel, F. Zuleger / Talk: 30th European Symposium on Programming (ESOP 2021), Luxembourg (online); 2021-03-27 - 2021-04-01; in: "30th European Symposium on Programming, ESOP 2021", Springer, 12648 (2021), 664 - 692
- Eliminating Message Counters in Synchronous Threshold Automata / I. Stoilkovska, I. Konnov, J. Widder, F. Zuleger / Talk: 22nd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), Copenhagen, Denmark; 2021-01-17 - 2021-01-19; in: "Proceedings of the 22nd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)", Springer LNCS, 12597 (2021), 196 - 218
- Rely-guarantee bound analysis of parameterized concurrent shared-memory programs / T. Pani, G. Weissenbacher, F. Zuleger / Formal Methods in System Design, 57 (2021), 2; 270 - 302
2020
- Thread-modular Counter Abstraction for Parameterized Program Safety / T. Pani, G. Weissenbacher, F. Zuleger / Talk: International Conference on Formal Methods in Computer-Aided Design (FMCAD), Haifa, Israel; 2020-09-22 - 2020-09-24; in: "Formal Methods in Computer-Aided Design", TU Wien Academic Press / IEEE, 1 (2020), ISBN: 978-3-85448-042-6; 67 - 76
- Multi-linear Strategy Extraction for QBF Expansion Proofs via Local Soundness / M. Schlaipfer, F. Slivovsky, G. Weissenbacher, F. Zuleger / Talk: International Conference on the Theory and Applications of Satisfiability Testing, Alghero, Italien; 2020-07-03 - 2020-07-10; in: "SAT 2020: Theory and Applications of Satisfiability Testing - SAT 2020", LNCS, 12178 (2020), ISBN: 978-3-030-51824-0; 429 - 446
- Beyond Symbolic Heaps: Deciding Separation Logic With Inductive Definitions / J. Pagel, F. Zuleger / in: "23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain", 73; EasyChair EPiC Series in Computing, 2020, 390 - 408
- The Polynomial Complexity of Vector Addition Systems with States / F. Zuleger / in: "Foundations of Software Science and Computation Structures - 23rd International Conference, Dublin, Ireland", 12077; Springer LNCS, 2020, 622 - 641
- Eliminating Message Counters in Threshold Automata / I. Stoilkovska, I. Konnov, J. Widder, F. Zuleger / in: "Automated Technology for Verification and Analysis - 18th Symposium, 2020, Hanoi, Vietnam", 12302; Springer LNCS, 2020, 196 - 212
2019
- Effective Entailment Checking for Separation Logic with Inductive Definitions / J. Pagel, C. Matheja, F. Zuleger / in: "25th International Conference, TACAS 2019", Springer, 2019, 319 - 336
- SL-COMP: Competition of Solvers for Separation Logic / M. Sighireanu, J. Pagel, C. Matheja, T. Noll, F. Zuleger et al. / in: "25th International Conference, TACAS 2019", Springer, 2019, 116 - 132
- Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking / I. Stoilkovska, I. Konnov, J. Widder, F. Zuleger / in: "International Conference on Tools and Algorithms for the Construction and Analysis of Systems", Springer, 2019, 357 - 374
2018
- Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms / T. Pani, G. Weissenbacher, F. Zuleger / Talk: International Conference on Formal Methods in Computer-Aided Design (FMCAD), Austin, TX; 2018-10-30 - 2018-11-02; in: "Formal Methods in Computer-Aided Design", FMCAD Inc., (2018), ISBN: 978-0-9835678-8-2; 1 - 9
- Using Loop Bound Analysis For Invariant Generation / P. Čadek, C. Danninger, M. Sinn, F. Zuleger / Talk: International Conference on Formal Methods in Computer-Aided Design (FMCAD), Austin, TX; 2018-10-30 - 2018-11-02; in: "Formal Methods in Computer-Aided Design", FMCAD Inc., (2018), ISBN: 978-0-9835678-8-2; 1 - 9
- Inductive Termination Proofs with Transition Invariants and Their Relationship to the Size-Change Abstraction / F. Zuleger / Talk: International Static Analysis Symposium (SAS), Freiburg, Germany; 2018-08-29 - 2018-08-31; in: "Static Analysis - 25th International Symposium, SAS 2018, Freiburg, Germany, August 29-31, 2018, Proceedings", Springer, Lecture Notes in Computer Science (2018), ISBN: 978-3-319-99724-7; 423 - 444
- Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS / T. Brazdil, K. Chatterjee, A. Kucera, P. Novotny, D. Velan, F. Zuleger / Talk: Symposium on Logic in Computer Science (LICS), Oxford; 2018-07-09 - 2018-07-12; in: "Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018", ACM, Oxford (2018), 185 - 194
- Automated clustering and program repair for introductory programming assignments / I. Radicek, S. Gulwani, F. Zuleger / Talk: Conference on Programming Language Design and Implementation (PLDI), Philadelphia, PA, USA; 2018-06-18 - 2018-06-22; in: "Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018", ACM, (2018), 465 - 480
- Monadic refinements for relational cost analysis / I. Radicek, G. Barthe, M. Gaboardi, D. Garg, F. Zuleger / Talk: 45th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2018), Los Angeles; 2018-01-10 - 2018-01-12; in: "Proceedings of the ACM on Programming Languages", ACM Digital Library, New York, NY, USA (2018), 1 - 32
- From Shapes to Amortized Complexity / T. Fiedor, L. Holik, A. Rogalewicz, M. Sinn, T. Vojnar, F. Zuleger / Talk: International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), Los Angeles; 2018-01-07 - 2018-01-09; in: "Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings", LNCS, 10747 (2018), ISBN: 978-3-319-73720-1; 205 - 225
- Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction / B. Aminof, I. Stoilkovska, S. Rubin, J. Widder, F. Zuleger / Talk: International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), Los Angeles; 2018-01-07 - 2018-01-09; in: "Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings", LNCS, 10747 (2018), ISBN: 978-3-319-73720-1; 1 - 24
- Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction / B. Aminof, S. Rubin, I. Stoilkovska, J. Widder, F. Zuleger / Talk: Verification, Model Checking, and Abstract Interpretation (VMCAI), Los Angeles; 2018-01-07 - 2018-01-09; in: "VMCAI", LNCS/Springer, 10747 (2018), 1 - 24
2017
- Automata and Program Analysis / L. Daviaud, T. Colcombet, F. Zuleger / Talk: Fundamentals of Computation Theory, Bordeaux, France (invited); 2017-09-11 - 2017-09-13; in: "Fundamentals of Computation Theory - 21st International Symposium, FCT 2017", (2017), 3 - 10
- Systematic Predicate Abstraction Using Variable Roles / Y. Demyanova, P. Rümmer, F. Zuleger / Talk: NASA Formal Methods (NFM), Moffett Field, CA, USA; 2017-05-16 - 2017-05-18; in: "NASA Formal Methods - 9th International Symposium, NFM 2017", (2017), 265 - 281
- Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic / J. Pagel, C. Jansen, F. Zuleger, C. Matheja, T. Noll / Talk: European Symposium on Programming (ESOP), Uppsala; 2017-04-22 - 2017-04-29; in: "Programming Languages and Systems - 26th European Symposium on Programming", (2017), 611 - 638
- On the Automated Verification of Web Applications with Embedded SQL / I. Shachar, T. Kotek, N. Rinetzky, M. Sagiv, O. Tamir, H. Veith, F. Zuleger / Talk: International Conference on Database Theory (ICDT), Venice, Italy; 2017-03-21 - 2017-03-24; in: "20th International Conference on Database Theory, ICDT 2017", (2017), 1 - 18
- Complexity and Resource Bound Analysis of Imperative Programs Using Difference Constraints / M. Sinn, H. Veith, F. Zuleger / Journal of Automated Reasoning, 59 (2017), 1; 3 - 45
- Empirical software metrics for benchmarking of verification tools / Y. Demyanova, T. Pani, H. Veith, F. Zuleger / Formal Methods in System Design, 50 (2017), 2; 289 - 316
2016
- Monadic Second Order Finite Satisfiability and Unbounded Tree-Width / T. Kotek, H. Veith, F. Zuleger / Talk: 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, Marseille; 2016-08-29 - 2016-09-01; in: "CSL", 62 (2016), ISBN: 978-3-95977-022-4; 1 - 20
- Automatic Verification of Multi-Agent Systems in Parameterised Grid-Environments / B. Aminof, A. Murano, S. Rubin, F. Zuleger / Talk: International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS), Singapur; 2016-05-09 - 2016-05-13; in: "AAMAS", (2016), 1190 - 1199
- Prompt Alternating-Time Epistemic Logics / B. Aminof, A. Murano, S. Rubin, F. Zuleger / Talk: 15th International Conference on Principles of Knowledge Representation and Reasoning (KR 2016), Kapstadt; 2016-04-25 - 2016-04-29; in: "KR", (2016), 258 - 267
2015
- On the Expressive Power of Communication Primitives in Parameterised Systems / B. Aminof, S. Rubin, F. Zuleger / Talk: Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), Suva, Fiji; 2015-11-24 - 2015-11-28; in: "LPAR", Springer, 9450 (2015), 313 - 328
- Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs / M. Sinn, H. Veith, F. Zuleger / Talk: International Conference on Formal Methods in Computer-Aided Design (FMCAD), Austin, Texas, USA; 2015-09-27 - 2015-09-30; in: "FMCAD", (2015), 144 - 151
- Empirical Software Metrics for Benchmarking of Verification Tools / Y. Demyanova, T. Pani, H. Veith, F. Zuleger / Talk: International Conference on Computer Aided Verification (CAV), San Francisco, CA, USA; 2015-07-18 - 2015-07-24; in: "CAV", Springer, 9206 (2015), ISBN: 978-3-319-21667-6; 561 - 579
- Asymptotically Precise Ranking Functions for Deterministic Size-Change Systems / F. Zuleger / Talk: International Computer Science Symposium in Russia (CSR), Listvyanka, Russia; 2015-07-13 - 2015-07-17; in: "CSR", Springer, 9139 (2015), 426 - 442
- Extending ALCQIO with Trees / T. Kotek, M. Simkus, H. Veith, F. Zuleger / Talk: 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2015), Kyoto, Japan; 2015-07-06 - 2015-07-10; in: "LICS 2015", IEEE, (2015), ISBN: 978-1-4799-8875-4; 511 - 522
- Liveness of Parameterized Timed Networks / B. Aminof, S. Rubin, F. Spegni, F. Zuleger / Talk: International Colloquium on Automata, Languages and Programming (ICALP), Kyoto, Japan; 2015-07-06 - 2015-07-10; in: "ICALP", Springer, 9135 (2015), 375 - 387
- Verification of Asynchronous Mobile-Robots in Partially-Known Environments / B. Aminof, A. Murano, S. Rubin, F. Zuleger / Talk: Principles and Practice of Multi-Agent Systems, Graz; 2015-05-18 - 2015-05-19; in: "PRIMA", Springer, 9387 (2015), 185 - 200
- Loop Patterns in C Programs / T. Pani, H. Veith, F. Zuleger / ECEASST, 72 (2015)
2014
- Feedback generation for performance problems in introductory programming assignments / S. Gulwani, I. Radicek, F. Zuleger / Talk: ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE), Hong Kong, China; 2014-11-16 - 2014-11-22; in: "FSE", ACM New York, NY, USA, (2014), ISBN: 978-1-4503-3056-5; 41 - 51
- Shape and Content - A Database-Theoretic Perspective on the Analysis of Data Structures / D. Calvanese, T. Kotek, M. Simkus, H. Veith, F. Zuleger / Keynote Lecture: International Conference in Integrated Formal Methods (IFM), Bertinoro, Italy (invited); 2014-09-09 - 2014-09-11; in: "IFM", Springer / LNCS, 8739 (2014), ISBN: 978-3-319-10180-4; 3 - 17
- Size-Change Abstraction and Max-Plus Automata / T. Colcombet, L. Daviaud, F. Zuleger / Talk: International Symposium on Mathematical Foundations of Computer Science (MFCS), Budapest, Ungarn; 2014-08-25 - 2014-08-29; in: "MFCS", Springer / LNCS, 8634 (2014), ISBN: 978-3-662-44521-1; 208 - 219
- A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis / M. Sinn, F. Zuleger, H. Veith / Talk: International Conference on Computer Aided Verification (CAV), Wien; 2014-07-18 - 2014-07-22; in: "CAV", Springer / LNCS, 8559 (2014), ISBN: 978-3-319-08866-2; 745 - 761
- Towards a Description Logic for Program Analysis: Extending ALCQIO with Reachability / T. Kotek, M. Simkus, H. Veith, F. Zuleger / Keynote Lecture: International Workshop on Description Logics, Wien; 2014-07-17 - 2014-07-20; in: "International Workshop on Description Logics", (2014), 4 pages
- Shape and Content: Incorporating Domain Knowledge into Shape Analysis / D. Calvanese, T. Kotek, M. Simkus, H. Veith, F. Zuleger / Talk: International Workshop on Description Logics, Wien; 2014-07-17 - 2014-07-20; in: "International Workshop on Description Logics", (2014), 4 pages
2013
- On the concept of variable roles and its use in software analysis / Y. Demyanova, H. Veith, F. Zuleger / Talk: International Conference on Formal Methods in Computer-Aided Design (FMCAD), Portland, OR, USA; 2013-10-20 - 2013-10-23; in: "FMCAD", IEEE, (2013), ISBN: 978-0-9835678-3-7; 226 - 230
- Ramsey vs. Lexicographic Termination Proving / B. Cook, A. See, F. Zuleger / Talk: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Rom, Italien; 2013-04-05 - 2013-04-13; in: "Tools and Algorithms for the Construction and Analysis of Systems", Lecture Notes in Computer Science. Springer Verlag., 7795 (2013), ISBN: 978-3-642-36741-0; 47 - 61
2011
- Bound Analysis of Imperative Programs with the Size-change Abstraction / F. Zuleger / Talk: Microsoft Research Lecture, Microsoft Research Cambridge, UK (invited); 2011-12-01
- Bound Analysis of Imperative Programs with the Size-change Abstraction / F. Zuleger / Talk: Theory Seminar, Queen Mary University, UK (invited); 2011-11-30
- Bound Analysis of Imperative Programs with the Size-change Abstraction / F. Zuleger / Talk: Austrian Society for Rigorous Systems Engineering (ARiSE) workshop together with PUMA workshop, Traunkirchen, Austria; 2011-10-03 - 2011-10-07
- Bound Analysis of Imperative Programs with the Size-change Abstraction / F. Zuleger, M. Sinn, S. Gulwani, H. Veith / Talk: International Static Analysis Symposium, Venice, Italy; 2011-09-14 - 2011-09-16; in: "Lecture Notes in Computer Science", E. Yahav (ed.); Springer, 6887 (2011), ISBN: 978-3-642-23701-0; 280 - 297
- Bound Analysis of Imperative Programs with the Size-change Abstraction / F. Zuleger / Talk: Software Systems Group Seminar, NICTA, Australien; 2011-07-19
- Resource bound analysis of imperative programs / Doctoral Thesis by F. Zuleger / Supervisor, Reviewer: H. Veith, S. Gulwani; Institut für Informationssysteme, 2011; oral examination: 2011-05-11
- Resource Bound Analysis of Imperative Programs / F. Zuleger / Talk: RiSE Seminar, Klosterneuburg; 2011-05-05
- Termination and Bound Analysis of Imperative Programs / F. Zuleger / Talk: Workshop on Logic and Computer Science, Vienna; 2011-03-24 - 2011-03-25
2010
- The reachability-bound problem / S. Gulwani, F. Zuleger / Talk: Conference on Programming Language Design and Implementation (PLDI), Toronto, Canada; 2010-06-05 - 2010-06-10; in: "PLDI'10 Proceedings of teh ACM SIGPLAN conference on Programming language design and implementation", B. G. Zorn, A. Aiken (ed.); PLDI'10 Proceedings of teh ACM SIGPLAN conference on Programming language design and implementation, (2010), ISBN: 978-1-4503-0019-3; 292 - 304
Supervisions
Note: Due to the rollout of TU Wien’s new publication database, the list below may be slightly outdated. Once APIs for the new database have been released, everything will be up to date again.
- SpecBMC : bounded model checker for speculative non-interference / Master Thesis by E. Pescosta / Supervisor: G. Weissenbacher, F. Zuleger; Logic and Computation, 2020
- Automated Complexity Analysis for Imperative Programs / Doctoral Thesis by M. Sinn / Supervisor, Reviewer: F. Zuleger, T. Vojnar; Institut für Informationssysteme, 2016
- Loop Patterns in C Programs / Master Thesis by T. Pani / Supervisor: F. Zuleger, H. Veith; Fakultät für Informatik der Technischen Universität Wien, 2013
Awards
-
Verication of Asynchronous Mobile-Robots in Partially-Known Environments
2015 / Best Paper Award / Italy
And more…
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 .