About - CV.pdf
positions: I am a researcher at the STU Bratislava. Before I did postdocs at the IST Austria under the direction of Thomas A. Henzinger, and at the IMDEA Software Institute under the direction of Pierre Ganty. I did my PhD at the ULB supervised by Emmanuel Filiot and Jean-François Raskin.
bio: My research interest lies in the domain of formal methods for computer-aided verification. I am focusing on specification models with a good tradeoff between the expressiveness of system behaviours and the complexity of algorithms that ensure safety and robustness.
keywords: formal methods, model-checking, monitoring, transducers, automata, logic, games.
Publications - DBLP
- Extending QuAK with Nested Quantitative Automata ( Arxiv, Proceedings ) Joint work with T. A. Henzinger, N. Ege Saraç, H. Yılmaz International Conference on Computer Aided Verification (CAV) 2026
- Kofola 1.0: A Modular Approach to omega-Regular Complementation and Inclusion Checking ( Arxiv, Proceedings ) Joint work with O. Alexaj, V. Havlena, L. Holík, O. Lengál, Y. Li International Conference on Computer Aided Verification (CAV) 2026
- Complementing Emerson-Lei Elevator Automata ( Arxiv, Proceedings ) Joint work with O. Alexaj, V. Havlena, O. Lengál, Y. Li International Conference on Concurrency Theory (CONCUR) 2026
- Temporal Explorability Games ( Arxiv, Proceedings ) Joint work with P. Austin, S. Bose, P. Totzke International Conference on Concurrency Theory (CONCUR) 2025
- Quantitative Language Automata ( Arxiv, Proceedings ) Joint work with Thomas A. Henzinger, N. Ege Saraç International Conference on Concurrency Theory (CONCUR) 2025
- Automating the Analysis of Quantitative Automata with QuAK ( Arxiv, Proceedings ) Joint work with Marek Chalupa, Thomas A. Henzinger, N. Ege Saraç International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2025
- Strategic Dominance: A New Preorder for Nondeterministic Processes ( Arxiv, Proceedings ) Joint work with Thomas A. Henzinger, N. Ege Saraç International Conference on Concurrency Theory (CONCUR) 2024
- QuAK: Quantitative Automata Kit ( Arxiv, Proceedings ) Joint work with Marek Chalupa, Thomas A. Henzinger, N. Ege Saraç International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISOLA) 2024
- Safety and Liveness of Quantitative Automata ( Arxiv, Proceedings, Journal ) Joint work with Udi Boker, Thomas A. Henzinger, and N. Ege Saraç International Conference on Concurrency Theory (CONCUR) 2023
- Regular Methods for Operator Precedence Languages ( Arxiv, Proceedings ) Joint work with Thomas A. Henzinger, Pavol Kebis and N. Ege Saraç International Colloquium on Automata, Languages and Programming (ICALP) 2023
- Quantitative Safety and Liveness ( Arxiv, Proceedings, Journal ) Joint work with Thomas A. Henzinger and N. Ege Saraç Journal Logical Methods in Computer Science (LMCS), Volume 21(2) International Conference on Foundations of Software Science and Computation Structures (FOSSACS) 2023
- Abstract Monitors for Quantitative Specifications ( Proceedings ) Joint work with Thomas A. Henzinger and N. Ege Saraç International Conference on Runtime Verification (RV) 2022
- FORQ-based Language Inclusion Formal Testing ( Arxiv, Proceedings ) Joint work with Kyveli Doveri and Pierre Ganty International Conference on Computer Aided Verification (CAV) 2022
- Decomposing Permutation Automata ( Arxiv, Proceedings, Journal ) Joint work with Ismaël Jecker and Petra Wolf Journal of Computer and System Sciences (JCSS), Volume 156 International Conference on Concurrency Theory (CONCUR) 2021
- Unary Prime Languages ( Proceedings ) Joint work with Ismaël Jecker and Orna Kupferman International Symposium on Mathematical Foundations of Computer Science (MFCS) 2020
- Weighted Transducers for Robustness Verification ( Proceedings ) Joint work with Emmanuel Filiot, Jean-François Raskin, Sriram Sankanarayanan and Ashutosh Trivedi International Conference on Concurrency Theory (CONCUR) 2020
- Two-way Parikh Automata ( Arxiv, Proceedings ) Joint work with Emmanuel Filiot and Shibashis Guha IARCS Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS) 2019
- Pattern Logic for Automata with Outputs ( Arxiv, Proceedings, Journal ) Joint work with Emmanuel Filiot and Jean-François Raskin International Journal of Foundations of Computer Science (IJFCS), Volume 31(6) International Conference on Developments in Language Theory (DLT) 2018
- Decidable Weighted Expressions with Presburger Combinators ( Arxiv, Proceedings, Journal ) Joint work with Emmanuel Filiot and Jean-François Raskin Journal of Computer and System Sciences (JCSS), Volume 106 International Symposium on Fundamentals of Computation Theory (FCT) 2017
Theses
- Contributions to formalisms for the specification and verification of quantitative properties (PDF) advised by E. Filiot and J.-F. Raskin Doctoral thesis, Univertié libre de Bruxelles BELGIUM, 2020
- The Complexity of Sum Automata Expressions with Lipschitz Robustness Application (PDF) advised by E. Filiot and J.-F. Raskin Master thesis, ENS Cachan FRANCE, 2016
- Uniformisation des relations automatiques par transducteur subséquentiel (PDF) advised by C. Löding Master thesis, ENS Cachan FRANCE, 2015
Talks
- i3S invited seminar 2025 in Sophia Antipolis
- GT Vérif 2025 keynote speaker in Créteil
- ISTA invited seminar 2025 in Klosterneuburg
- VUT FIT invited seminar 2025 in Brno
- 34th International Conference TACAS 2025 in Hamilton (slides)
- Université de Franche-Conté invited seminar in Besançon
- UMONS invited seminar in Mons
- 12th European conference Highlights of Logic, Games, and Automata 2024 in Bordeaux (slides)
- VUT FIT invited seminar 2024 in Brno
- 35th International Conference CONCUR 2024 in Calgary (slides)
- University of Liverpool invited seminar 2023 in Liverpool
- 34th International Conference CONCUR 2023 in Antwerp (slides)
- STU invited seminar 2023 in Bratislava
- 50th International Conference ICALP 2023 in Paderborn (slides)
- ISTA/FORSYTE shared-seminar 2022 in Klosterneuburg
- 22nd International Conference RV 2022 online (slides)
- ISTA invited seminar 2021 in Klosterneuburg
- 32st International Conference CONCUR 2021 online (slides, video, poster)
- IMDEA Software Seminar Series 2021 in Madrid
- PhD defence 2020 online
- 31st International Conference CONCUR 2020 online (slides)
- University of Colorado Boulder invited seminar 2020 online
- 39th IARCS Annual Conference FSTTCS 2019 in Mumbai (slides)
- 7th European conference Highlights of Logic, Games and Automata 2019 in Warsaw (slides)
- 6th European conference Highlights of Logic, Games and Automata 2018 in Berlin (slides)
- 22nd International Symposium DLT 2018 in Tokyo (slides)
- ISTA invited seminar 2018 in Klosterneuburg
- 2nd Winter School in Engineering and Computer Science 2017 in Jerusalem
- 5th European conference Highlights of Logic, Games and Automata 2017 in London (slides)
- 21st International Symposium FCT 2017 in Bordeaux (slides)
Software
- QuAK (GitHub, Zenodo) Quantitative automata library for safety-liveness monitoring, checker, and synthesizer Peer-reviewed by TACAS 2025 artifact committee (Proceedings)
- FORKLIFT (GitHub, Zenodo) Büchi automata Ramsey-based language inclusion checker with antichain heuristics Peer-reviewed by CAV 2022 artifact committee (Proceedings)
Teaching
- IST Austria 2023
- Foundation of Model Checking (slides, exercices and solutions on ISTA Athena)
- Université libre de Bruxelles 2020
- INFO-F412 - Formal verification of computer systems ( Mickael Randour's webpage )
- Université libre de Bruxelles 2019
- INFO-F412 - Formal verification of computer systems ( Mickael Randour's webpage )
- INFO-F410 - Embedded Systems Design ( ULB Université Virtuelle )
- Université libre de Bruxelles 2018
- INFO-F412 - Formal verification of computer systems ( Mickael Randour's webpage )
- INFO-F410 - Embedded Systems Design ( ULB Université Virtuelle )
- INFO-F302 - Informatique Fondamentale ( lecture webpage )
- Université libre de Bruxelles 2017
- INFO-F412 - Formal verification of computer systems ( Mickael Randour's webpage )
Miscellaneous
- Viennese workshop on Verification 2023 main organizer (35 participants, 28 speakers)
- RP'19 organizer assitant (80 participants, 34 speakers)