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

Contact

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

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