Perun: Light-weight Performance Version System
An open source light-weight Performance Version System and tool suite of performance analysis and profiling tools.
Tags: fuzz testing, performance analysis, performance testing, profiling, tool suite
An open source light-weight Performance Version System and tool suite of performance analysis and profiling tools.
Tags: fuzz testing, performance analysis, performance testing, profiling, tool suite
Mata is an open source automata library that offers interface for different kinds of automata (NFA).
Tags: finite automata, library
Gaston is an implementation of backward decision procedure logic for WS1S logic.
Tags: decision procedure, nondeterministic finite automata, ws1s
This paper is our initial work on deciding WS1S logic using non-deterministic finite automata
FIEDOR Tomáš, HOLÍK Lukáš, LENGÁL Ondřej and VOJNAR Tomáš. Nested Antichains for WS1S. In: Proceedings of TACAS'15. Lecture Notes in Computer Science, vol. 9035. Heidelberg: Springer Verlag, 2015, pp. 658-674. ISBN 978-3-662-46680-3.
Tags: anti-chains, decision procedures, nondeterministic finite automata, ws1s logic
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.
Tags: anti-chains, decision procedures, lazy techniques, nondeterministic finite automata, ws1s logic
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.
Tags: amortized complexity, complexity analysis, heap-manipulating programs, performance analysis, shape analysis
This is an extended journal version of our TACAS’15 paper
FIEDOR Tomáš, HOLÍK Lukáš, LENGÁL Ondřej and VOJNAR Tomáš. Nested Antichains for WS1S. Acta Informatica, vol. 56, no. 3, 2019, pp. 205-228. ISSN 0001-5903.
Tags: antichains, decision procedures, nondeterministic finite automata, ws1s logic
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.
Tags: fuzztesting, performance analysis, performance testing, profiling, version system
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.
Tags: alternating automata, benchmarking, finite automata, regular properties, smt solvers
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
Tags: automata library, c++, finite automata, python
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.
The goal of this thesis was to create a memory profiler of C/C++. The results were interpretered using several kinds of visualizations: (1) heat maps (both in GUI and in CLI using ncurses
library), and (2) flamegraphs.
Tags: memory, performance testing, perun
Disclaimer: This thesis was supervised together with RedHat company; I served mainly as a formal superviser; technical consultant were Stanislav Židek and Hubert Kario. The goal of the thesis was to extend the capabilities of testing attacks based on fuzztesting solved within the RedHat company.
The goal of this thesis was to create a graphical user interface for my Perun project. The GUI was realized based on modern approaches to website development using vue.js
framework. The GUI is, however, currently outdated and not merged in our upstream.
Tags: gui, performance testing, perun
Disclaimer: This thesis was supervised together with RedHat company; I served mainly as a formal supervisor; technical consultants were Zdeněk Kraus and Otavio Rodolfo Piske. This thesis goal was to extend the capabilities of performance testing conducted in Red Hat company.
Tags: external, network analysis, performance testing, redhat
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: fuzzing, performance fuzzing, perun
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: infer, loopus, resource bounds analysis, static analysis
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: performance modelling, performance regression analysis, perun
The goal of this work was to optimize the profiling time and space based on several aspects of projects or profiling process: based on structure of the profiled program, based on complexity of the analysed functions, or recency of the changes. This is without doubt, my most favourite work I have supervised.
Tags: optimization, perun, profiling
The goal of this thesis was to extend the capabilities of Perun with injecting noise into program to either simulate potential code optimisations or to make performance issues manifest during profiling.
Tags: noise injection, performance analysis, performance blowing
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 trace
profiler with support for PIN framework. This would allow us to overcome some of the limitations of our current underlying instrumentation frameworks (eBPF and SystemTap).
Tags: basic block analysis, PIN, profiling
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: , perun, profiling, scatter plot, tree map
Disclaimer: This thesis was mainly supervised by Ing. Jiří Pavela; I have served as additional technical consultant. The goal of this thesis was to experimentally try to measure the consumption of the energy of profiled programs.
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:
Published:
This was presentation of our paper accepted ad TACAS’15.
Tags:
Published:
This was presentation of our paper accepted ad TACAS’15 during the Alpine Verification Meeting.
Tags:
Published:
This was presentation of our paper accepted ad TACAS’15 during the MEMICS 2015 local conference.
Tags:
Published:
This was presentation of formal analysis and verification group.
Tags:
Published:
This was presentation of advancements of my formal analysis research, which was partly funded by Red Hat company.
Tags:
Published:
This was presentation of advancements of my formal analysis research, which was partly funded by Red Hat company.
Tags:
Published:
This was presentation of our paper accepted ad TACAS’17.
Tags:
Published:
This was presentation of our paper accepted ad VMCAI’18.
Tags:
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:
Published:
This was presentation of advancements of my performance analysis research, which was partly funded by Red Hat company.
Tags:
Published:
This was an internal seminary talk on perform experimental evaluation of ones research. The talk is private and the slides will not be available (it could contain some unwanted jokes; and some sensitive informations).
Tags:
Published:
This was an internal seminary talk on how to write better. The talk is private and the slides will not be available (it could contain some unwanted jokes).
Tags:
Published:
This was an internal seminary talk on how AI, its usage and some issues. The talk is private and the slides will not be available (it could contain some unwanted jokes).
Tags:
Published:
This was an accepted talk at DevConf’24 and presented cooperation between BUT FIT (mainly by me and my colleague Jirka Pavela) with RedHat (Kernel Performance Team led by Jirka Hladký).
Tags: