Florian Zuleger
Address:
Florian Zuleger
Technische Universität Wien
Institut für Logic and Computation 192/4
Favoritenstraße 9–11
1040 Wien
Austria
| Room: | HG 03 09 (how to get there) |
| Phone: | +43 (1) 58801 – 184 49 |
| Email: | zuleger@forsyte.at |
| Web: | http://forsyte.at/~zuleger/ |
Teaching
- 183.703 Program Analysis.
-
184.749 Semantics of Programming Languages.
I’m offering student projects, click here, here and here for more information.
Publications
extended version of SAS 2011 paper
| 2020 | |
| [38] | Rely-Guarantee Bound Analysis of Parameterized Concurrent Shared-Memory Programs , 2020. Note: under submission |
| [37] | Thread-modular Counter Abstraction for Parameterized Program Safety Formal Methods in Computer Aided Design, FMCAD (Alexander Ivrii, Ofer Strichman, eds.), 2020. Note: to appear |
| 2019 | |
| [36] | Verifying Safety of Synchronous Fault-Tolerant Algorithms Bounded Model Checking Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part II, pages 357–374, 2019. Note: A pre-print including the proofs is available at: https://hal.inria.fr/hal-01925653 |
| 2018 | |
| [35] | Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking HAL, volume hal-01925653, Nov 2018. Note: Accepted at TACAS 2019 |
| [34] | Monadic refinements for relational cost analysis POPL 2018, 2018. Note: (to appear) |
| [33] | Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms Formal Methods in Computer Aided Design, FMCAD (Nikolaj Bjørner, Arie Gurfinkel, eds.), pages 1–9, 2018, IEEE. |
| [32] | Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings (Isil Dillig, Jens Palsberg, eds.), volume 10747 of Lecture Notes in Computer Science, pages 1–24, 2018, Springer. |
| 2017 | |
| [31] | Complexity and Resource Bound Analysis of Imperative Programs Using Difference Constraints Journal of Automated Reasoning, pages 1–43, 2017. |
| [30] | Empirical software metrics for benchmarking of verification tools Formal Methods in System Design, volume 50, number 2-3, pages 289–316, 2017. |
| 2016 | |
| [29] | A simple and scalable static analysis for bound analysis and amortized complexity analysis Software Engineering 2016, Fachtagung des GI-Fachbereichs Softwaretechnik, 23.-26. Februar 2016, Wien, Österreich, pages 101–102, 2016. |
| [28] | Prompt Alternating-Time Epistemic Logics Principles of Knowledge Representation and Reasoning: Proceedings of the Fifteenth International Conference, KR 2016, Cape Town, South Africa, April 25-29, 2016., pages 258–267, 2016. |
| [27] | Monadic Second Order Finite Satisfiability and Unbounded Tree-Width 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France, pages 13:1–13:20, 2016. |
| [26] | Automatic Verification of Multi-Agent Systems in Parameterised Grid-Environments Proceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems, Singapore, May 9-13, 2016, pages 1190–1199, 2016. |
| [25] | Automated Clustering and Program Repair for Introductory Programming Assignments CoRR, volume abs/1603.03165, 2016. |
| [24] | Feedback generation for performance problems in introductory programming assignments Software Engineering 2016, Fachtagung des GI-Fachbereichs Softwaretechnik, 23.-26. Februar 2016, Wien, Österreich, pages 49–50, 2016. |
| [23] | Empirical software metrics for benchmarking of verification tools Software Engineering 2016, Fachtagung des GI-Fachbereichs Softwaretechnik, 23.-26. Februar 2016, Wien, Österreich, pages 67–68, 2016. |
| 2015 | |
| [22] | Empirical Software Metrics for Benchmarking of Verification Tools Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, pages 561–579, July 2015. |
| [21] | Extending ALCQIO with Trees 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 511–522, 2015. |
| [20] | Verification of Asynchronous Mobile-Robots in Partially-Known Environments PRIMA 2015: Principles and Practice of Multi-Agent Systems - 18th International Conference, Bertinoro, Italy, October 26-30, 2015, Proceedings, volume 9387 of Lecture Notes in Computer Science, pages 185–200, 2015, Springer. |
| [19] | On the Expressive Power of Communication Primitives in Parameterised Systems Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings, volume 9450 of Lecture Notes in Computer Science, pages 313–328, 2015, Springer. |
| [18] | Liveness of Parameterized Timed Networks Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II, volume 9135 of Lecture Notes in Computer Science, pages 375–387, 2015, Springer. |
| [17] | Asymptotically Precise Ranking Functions for Deterministic Size-Change Systems Computer Science - Theory and Applications - 10th International Computer Science Symposium in Russia, CSR 2015, Listvyanka, Russia, July 13-17, 2015, Proceedings, volume 9139 of Lecture Notes in Computer Science, pages 426–442, 2015, Springer. |
| [16] | Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs Formal Methods in Computer-Aided Design (FMCAD) (Roope Kaivola, Thomas Wahl, eds.), pages 144-151, 2015, IEEE. |
| [15] | Loop Patterns in C Programs ECEASST, volume 72, 2015. |
| 2014 | |
| [14] | Feedback Generation for Performance Problems in Introductory Programming Assignments ArXiv e-prints, volume abs/1403.4064, March 2014. Note: technical report/extended version of FSE14 paper |
| [13] | Towards a Description Logic for Program Analysis: Extending ALCQIO with Reachability Informal Proceedings of the 27th International Workshop on Description Logics, Vienna, Austria, July 17-20, 2014., pages 591–594, 2014. |
| [12] | Shape and Content: Incorporating Domain Knowledge into Shape Analysis Informal Proceedings of the 27th International Workshop on Description Logics, Vienna, Austria, July 17-20, 2014., pages 124–127, 2014. |
| [11] | A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis Chapter in Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, pages 745–761, 2014. |
| [10] | Feedback Generation for Performance Problems in Introductory Programming Assignments Proceedings of the 22Nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, pages 41–51, 2014, ACM. |
| [9] | Size-Change Abstraction and Max-Plus Automata Mathematical Foundations of Computer Science 2014 - 39th International Symposium, MFCS 2014, Budapest, Hungary, August 25-29, 2014. Proceedings, Part I, pages 208–219, 2014. |
| [8] | Shape and Content - A Database-Theoretic Perspective on the Analysis of Data Structures Integrated Formal Methods - 11th International Conference, IFM 2014, Bertinoro, Italy, September 9-11, 2014, Proceedings, pages 3–17, 2014. |
| 2013 | |
| [7] | On the Concept of Variable Roles and its Use in Software Analysis ArXiv e-prints, volume abs/1305.6745, May 2013. |
| [6] | Ramsey vs. Lexicographic Termination Proving TACAS, pages 47-61, 2013. |
| [5] | On the Concept of Variable Roles and its Use in Software Analysis FMCAD, pages 226–229, 2013. |
| 2011 | |
| [4] | Bound analysis of imperative programs with the size-change abstraction Proceedings of the 18th international conference on Static analysis, pages 280–297, 2011, Springer-Verlag. |
| 2010 | |
| [3] | Loopus - A Tool for Computing Loop Bounds for C Programs Proceedings of the 3rd Workshop on Invariant Generation (WING), 2010. |
| [2] | The reachability-bound problem PLDI, pages 292-304, 2010. |
| 2009 | |
| [1] | An Abstract Interpretation-Based Framework for Control Flow Reconstruction from Binaries Proceedings of the Tenth International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2009) (Neil D. Jones, Markus Müller-Olm, eds.), volume 5403 of Lecture Notes in Computer Science, January 2009, Springer. |
