Page Not Found
Page not found. Your pixels are in another canvas.
Sitemap
A list of all the posts and pages found on the site. For you robots out there is an XML version available for digesting as well.
Pages
Page not in menu
This is a page not in th emain menu
Posts
Blog Post number 1
Published:
This is a sample blog post. Lorem ipsum I can’t remember the rest of lorem ipsum and don’t have an internet connection right now. Testing testing testing this blog post. Blog posts are cool.
projects
Perun: Light-weight Performance Version System
An open source light-weight Performance Version System and tool suite of performance analysis and profiling tools.
Mata: The Automata Library
Mata is an open source automata library that offers interface for different kinds of automata (NFA).
Gaston: Decision Procedure for WS1S Logic
Gaston is an implementation of backward decision procedure logic for WS1S logic.
publications
Nested Antichains for 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
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.
Tags: anti-chains, decision procedures, lazy techniques, nondeterministic finite automata, ws1s logic
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.
Tags: amortized complexity, complexity analysis, heap-manipulating programs, performance analysis, shape analysis
Nested Antichains for WS1S
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
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.
Tags: fuzztesting, performance analysis, performance testing, profiling, version system
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.
Tags: alternating automata, benchmarking, finite automata, regular properties, smt solvers
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.
Radim Podola: Library for Profiling and Visualization of Memory Consumption of C/C++ Programs
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.
Milan Lysoňek: Existing Attacks on SSL/TLS Protocol
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.
Martina Grzybowská: Graphical User Interface for Performance Control System
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.
Jakub Stejskal: Performance Testing and Analysis of Qpid Dispatch Router
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.
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).
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.
Š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.
Jiří Pavela: Efficient Techniques for Program Performance 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 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.
Matúš Liščinský: Performance Analysis Based on Noise Injection
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.
Peter Močáry: Performance Analysis of Programs Based on PIN Framework
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).
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.
Ondřej Míchal: Analysis of Software Resource Consumption
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.
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.
Nested Antichains for WS1S
Published:
This was presentation of our paper accepted ad TACAS’15.
Nested Antichains for WS1S
Published:
This was presentation of our paper accepted ad TACAS’15 during the Alpine Verification Meeting.
Nested Antichains for WS1S
Published:
This was presentation of our paper accepted ad TACAS’15 during the MEMICS 2015 local conference.
VeriFIT: Automatic analysis and verification
Published:
This was presentation of formal analysis and verification group.
Formal Analysis and Verification of Program Termination and Resource Bounds
Published:
This was presentation of advancements of my formal analysis research, which was partly funded by Red Hat company.
Formal Analysis and Verification of Program Termination and Resource Bounds
Published:
This was presentation of advancements of my formal analysis research, which was partly funded by Red Hat company.
Lazy Automata Techniques for WS1S
Published:
This was presentation of our paper accepted ad TACAS’17.
From Shapes to Amortized Complexity
Published:
This was presentation of our paper accepted ad VMCAI’18.
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).
Perun: Performance Under Control
Published:
This was presentation of advancements of my performance analysis research, which was partly funded by Red Hat company.
The Sins, The Confessions and The Repentance: The autopsy of the modern experimental evaluation.
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).
The Bollocks, The Revisions and The Elegance: The autopsy of the modern (technical) writing
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).
The Rise of Machines, the Fall of Humanity, and Other Good Times: The autopsy of the modern (artificial) intelligence
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).