Posts by Collection

projects

publications

Lazy Automata Techniques for WS1S

This paper is our follow-up work on deciding WS1S logic using non-deterministic finite automata

FIEDOR Tomáš, HOLÍK Lukáš, JANKŮ Petr, LENGÁL Ondřej and VOJNAR Tomáš. Lazy Automata Techniques for WS1S. In: Proceedings of TACAS'17. Lecture Notes in Computer Science, vol. 10205. Heidelberg: Springer Verlag, 2017, pp. 407-425. ISBN 978-3-662-54576-8. ISSN 0302-9743.

TACAS, 2017.

Tags: , , , ,

From Shapes to Amortized Complexity

This paper is our work automatic complexity analysis of programs manipulating with dynamic data structures.

FIEDOR Tomáš, HOLÍK Lukáš, ROGALEWICZ Adam, SINN Moritz, VOJNAR Tomáš and ZULEGER Florian. From Shapes to Amortized Complexity. In: Proceedings of VMCAI'18. Lecture Notes in Computer Science, vol. 10145. Heidelberg: Springer Verlag, 2018, pp. 205-225. ISBN 978-3-319-73720-1. ISSN 0302-9743.

VMCAI, 2018.

Tags: , , , ,

Perun: Performance Version System

This tool paper introduces our Perun tool suite on series of case studies of real performance issues

FIEDOR Tomáš, PAVELA Jiří, ROGALEWICZ Adam and VOJNAR Tomáš. Perun: Performance Version System. In: Proceedings of the 38th IEEE International Conference on Software Maintenance and Evolution (ICSME 2022). Limassol: Institute of Electrical and Electronics Engineers, 2022, pp. 499-503. ISBN 978-1-6654-7956-1.

ICSME, 2022.

Tags: , , , ,

Reasoning about Regular Properties: A Comparative Study

This paper is a comparative study of several different approaches to reasoning about regular properties.

FIEDOR Tomáš, HOLÍK Lukáš, HRUŠKA Martin, ROGALEWICZ Adam, SÍČ Juraj and VARGOVČÍK Pavol. Reasoning about Regular Properties: A Comparative Study. In: Automated Deduction - CADE 29. Cham: Springer Nature Switzerland AG, 2023, pp. 286-306. ISSN 0302-9743.

CADE, 2023.

Tags: , , , ,

Mata: A Fast and Simple Finite Automata Library

This paper is a tool paper about efficient automata library written in C++ with Python binding.

CHOCHOLATÝ, David, FIEDOR Tomáš, HAVLENA Vojtěch, HOLÍK Lukáš, HRUŠKA Martin, LENGÁL Ondřej, SÍČ Juraj. Mata: A Fast and Simple Finite Automata Library. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems - TACAS'24. Lecture Notes in Computer Science, vol 14571. Springer, Cham

TACAS, 2024.

Tags: , , ,

students

Jiří Pavela: Library for Profiling of Data Structures of C/C++ Programs

The goal of this thesis was to create a time profiler of C/C++ programs together with tracking sizes of advanced data structures (such as linked lists or skip lists). The collected data was postprocessed using regression analysis to infer mathematical models (which modeled runtime of functions based on sizes of underlying structures). The results were visualized using scatter plots.

Tags: , ,

Matúš Liščinský: Fuzz Testing of Program Performance

Disclaimer: While this thesis was officially supervised by Adam Rogalewicz (due some internal restrictions), I was the main supervisor of this whole thesis. The goal of this thesis was to extend the notion of performance fuzztesting to more fine-tuned (custom) rules and more performance-based evaluation. The resulting fuzzer is part of Perun and provides new ideas (sadly unpublished).

Tags: , ,

Ondřej Pavela: Static Analysis Using Facebook Infer Focused on Performance Analysis

Disclaimer: This thesis was supervised by Tomáš Vojnar, I was the technical consultant. The goal of this thesis was build upon our work on automatic complexity analysis; this was initial work that only had to reproduce the results of Loopus tools invented by our colleagues in TU Vienna (Moritz Sinn and Florian Zuleger) in the Facebook Infer framework.

Tags: , , ,

Šimon Stupinský: New Models for Automatic Detection of Performance Degradation

Disclaimer: While this thesis was officially supervised by Adam Rogalewicz (due some internal restrictions), I was the main supervisor of this whole thesis. The goal of this thesis was to extend the capabilities of Perun with new models (besides so-far supported regression analysis) as well as new approaches to detect performance degradations in software. In particular, we come up with non-parametric models (models not dependent on other variables) such as regressograms, moving averages or kernel regressions; as well as methods for detecting performance issues based on integral computation or local statistics.

Tags: , ,

Vojtěch Hájek: Performance Analysis of C# Programs

Disclaimer: This thesis was mainly supervised by Ing. Jiří Pavela; I have served as additional technical consultant. The goal of this thesis was to extend our profilers with profiler for programs written in C#, potentially extending our support for Windows (sub)systems. The results were interpreted using tree-like views similar to outputs of kcachegrind.

Tags: , , , ,

talks

Nested Antichains for WS1S

Published:

This was presentation of our paper accepted ad TACAS’15 during the Seminary talk in Charles University, Faculty of Mathematics and Physics, in Prague, where I was invited.

Tags:

Nested Antichains for WS1S

Published:

This was presentation of our paper accepted ad TACAS’15 during the Alpine Verification Meeting.

Tags:

Nested Antichains for WS1S

Published:

This was presentation of our paper accepted ad TACAS’15 during the MEMICS 2015 local conference.

Tags:

Perun: Performance Under Control

Published:

This was an internal seminary talk about Perun project. The talk is private and the slides will not be available (it could contain some unwanted jokes).

Tags:

Perun: Performance Under Control

Published:

This was presentation of advancements of my performance analysis research, which was partly funded by Red Hat company.

Tags: