Automated Program Analysis for Bounds on Resource Consumption

Resource Bound Analysis

Computer programs are consuming physical resources such as time, memory, power and bandwidth. To guarantee that a program only uses a limited amount of these resources, programmers need automatic tools which predict the resource consumption of a program. We investigate theoretical frameworks that allow to model and analyze the complexity of programs and build practical program analysis tools that allow to infer bounds on the resource consumption of the program under analysis.

Feedback Generation for Introductory Programming Problems

Providing feedback on programming assignments is an integral part of a class on introductory programming and requires substantial effort by the teaching personnel. This problem has become even more significant today with the increasing popularity of programming education. We investigate automated methods for generating feedback on introductory programming assignments.

Liveness Properties of Parameterized Systems

Parameterized systems consist of an arbitrary number of replications of the same system component. The challenge is to verify the correctness of such systems for all possible system sizes. Results on the decidability of such systems are scarce and have mostly been obtained for safety properties. We investigate the decidability of liveness properties and study how to obtain quantitative measures for the progress of the system.

Recent papers

2016
[18] Prompt Alternating-Time Epistemic Logics
Benjamin Aminof, Aniello Murano, Sasha Rubin, Florian Zuleger
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.
[bibtex] [pdf]
[17] Automatic Verification of Multi-Agent Systems in Parameterised Grid-Environments
Benjamin Aminof, Aniello Murano, Sasha Rubin, Florian Zuleger
Proceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems, Singapore, May 9-13, 2016, pages 1190-1199, 2016.
[bibtex] [pdf]
2015
[16] Empirical Software Metrics for Benchmarking of Verification Tools
Yulia Demyanova, Thomas Pani, Helmut Veith, Florian Zuleger
Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, pages 561-579, July 2015.
[bibtex] [pdf] [doi]
[15] Extending ALCQIO with Trees
Tomer Kotek, Mantas Simkus, Helmut Veith, Florian Zuleger
30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 511-522, 2015.
[bibtex] [pdf] [doi]
[14]Verification of Asynchronous Mobile-Robots in Partially-Known Environments
Sasha Rubin, Florian Zuleger, Aniello Murano, Benjamin Aminof
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.
[bibtex] [doi]
[13]On the Expressive Power of Communication Primitives in Parameterised Systems
Benjamin Aminof, Sasha Rubin, Florian Zuleger
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.
[bibtex] [doi]
[12]Liveness of Parameterized Timed Networks
Benjamin Aminof, Sasha Rubin, Florian Zuleger, Francesco Spegni
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.
[bibtex] [doi]
[11]Asymptotically Precise Ranking Functions for Deterministic Size-Change Systems
Florian Zuleger
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.
[bibtex] [doi]
[10]Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs
Moritz Sinn, Florian Zuleger, Helmut Veith
Formal Methods in Computer-Aided Design (FMCAD) (Roope Kaivola, Thomas Wahl, eds.), pages 144-151, 2015, IEEE.
[bibtex]
[9] Loop Patterns in C Programs
Thomas Pani, Helmut Veith, Florian Zuleger
ECEASST, volume 72, 2015.
[bibtex] [pdf]
2014
[8]Towards a Description Logic for Program Analysis: Extending ALCQIO with Reachability
Tomer Kotek, Mantas Simkus, Helmut Veith, Florian Zuleger
Informal Proceedings of the 27th International Workshop on Description Logics, Vienna, Austria, July 17-20, 2014., pages 591-594, 2014.
[bibtex]
[7]Shape and Content: Incorporating Domain Knowledge into Shape Analysis
Diego Calvanese, Tomer Kotek, Mantas Simkus, Helmut Veith, Florian Zuleger
Informal Proceedings of the 27th International Workshop on Description Logics, Vienna, Austria, July 17-20, 2014., pages 124-127, 2014.
[bibtex]
[6] A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis
Moritz Sinn, Florian Zuleger, Helmut Veith
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.
[bibtex] [pdf] [doi]
[5] Feedback Generation for Performance Problems in Introductory Programming Assignments
Sumit Gulwani, Ivan Radiček, Florian Zuleger
Proceedings of the 22Nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, pages 41-51, 2014, ACM.
[bibtex] [pdf] [doi]
[4] Size-Change Abstraction and Max-Plus Automata
Thomas Colcombet, Laure Daviaud, Florian Zuleger
Mathematical Foundations of Computer Science 2014 - 39th International Symposium, MFCS 2014, Budapest, Hungary, August 25-29, 2014. Proceedings, Part I, pages 208-219, 2014.
[bibtex] [pdf] [doi]
[3] Shape and Content - A Database-Theoretic Perspective on the Analysis of Data Structures
Diego Calvanese, Tomer Kotek, Mantas Simkus, Helmut Veith, Florian Zuleger
Integrated Formal Methods - 11th International Conference, IFM 2014, Bertinoro, Italy, September 9-11, 2014, Proceedings, pages 3-17, 2014.
[bibtex] [pdf] [doi]
2013
[2]Ramsey vs. Lexicographic Termination Proving
Byron Cook, Abigail See, Florian Zuleger
TACAS, pages 47-61, 2013.
[bibtex]
[1] On the Concept of Variable Roles and its Use in Software Analysis
Yulia Demyanova, Helmut Veith, Florian Zuleger
FMCAD, pages 226-229, 2013.
[bibtex] [pdf]

Contact

Address:
Florian Zuleger
Technische Universität Wien
Institut für Informationssysteme 184/4
Favoritenstraße 9–11
1040 Wien
Austria

Room: HG 03 09 (how to get there)
Phone: +43 (1) 58801 – 184 49
Email: ta.etysrofnull@regeluz
Web: http://forsyte.at/~zuleger/

Latest News

Opening of Vienna Center for Logic and Algorithms (VCLA) on Jan 25

The Vienna Center for Logic and Algorithms is an initiative of the Faculty of Informatics and funded by a three-year competitive grant of Vienna University of Technology. Embedded into the primary research area Computational Intelligence and the funding priority Computational Logic of the Faculty, the center is promoting international scientific collaboration in logic and algorithms. […]

Continue reading

Winter School on Verification

The Austrian Society for Rigorous Systems Engineering (ARiSE) and the Vienna Center for Logic and Algorithms (VCLA) are organizing a joint winter school on verification at Vienna University of Technology from 6-10 February 2012. Apart from ARiSE/VCLA students, the school will be open to outside students. Details are available from the VCLA website.

Continue reading

CfP: Workshop on Exploiting Concurrency Efficiently and Correctly (EC^2 2010)

The annual Workshop on Exploiting Concurrency Efficiently and Correctly (EC2) is a forum that brings together researchers working on formal methods for concurrency, and those working on advanced parallel applications. Its goal is to stimulate incubation of ideas leading to future concurrent system design an verification tools that are essential in the multi-core era.

Continue reading

Full news archive