Contact
- Email: fandikb [at] gmail.com
- Post:
UMONS - Faculty of Science - Mathematics Department,
Bâtiment De Vinci, Avenue Victor Maistriau, 23,
7000 Mons,
BELGIUM
Research
My research interests are LTL to ω-automata translations, model-checking, control synthesis, formal verification for software analysis.
My thesis is titled Automata for Formal Methods: Little Steps Towards Perfection and was reviewed by Orna Kupferman and Christel Baier [submitted, corrected, and ready-to-print corrected versionsi, list of fixes].
Projects
- LTL3DRA
Translation of LTL-GUX into deterministic automata
- HOAF
Format for exchanging ω-automata
- LTL3TELA
Translation of LTL to transition-based Emerson-Lei automata
- Seminator
Semi-determinization of generalized Büchi automata
Proceedings publications
-
F. Blahoudek, J. Major, and J. Strejcek:
LTL to Smaller Self-Loop Alternating Automata and Back,
in Proceedings of ICTAC 2019, LNCS, Springer, 2019. To appear.
-
Ch. Baier, F. Blahoudek, A. Duret-Lutz, J. Klein, D. Mueller, and J. Strejcek:
Generic Emptiness Check for Fun and Profit,
in Proceedings of ATVA 2019, LNCS, Springer, 2019. To appear.
[extended version PDF]
-
J. Major, F. Blahoudek, J. Strejcek, M. Sasarakova, and T. Zboncakova:
ltl3tela: LTL to Small Deterministic or Nondeterministic Emerson-Lei Automata,
in Proceedings of ATVA 2019, LNCS, Springer, 2019. To appear.
[preprint PDF]
-
F. Blahoudek, A. Duret-Lutz, M. Klokočka, M. Křetínský, and J. Strejček:
Seminator: A Tool for Semi-Determinization of Omega-Automata,
in Proceedings of LPAR 2017, EPiC Series in Computing 46, pages 356-367, 2017.
[link,
PDF]
-
F. Blahoudek, M. Heizmann, S. Schewe, J. Strejček,
and M.-H. Tsai:
Complementing Semi-Deterministic Büchi Automata,
in Proceedings of TACAS 2016, volume 9636 of LNCS, pages 770-787. Springer-Verlag, 2016.
[DOI link,
preprint PDF]
-
F. Blahoudek, A. Duret-Lutz, V. Rujbr, and J. Strejček:
On Refinement of Büchi Automata for Explicit Model Checking,
in Proceedings of SPIN 2015, volume 9232 of LNCS. Springer-Verlag, 2015.
[DOI link,
preprint PDF,
corresponding data]
-
T. Babiak, F. Blahoudek, A. Duret-Lutz, J. Klein, J. Křetínský,
D. Mueller, D. Parker, and J. Strejček:
The Hanoi Omega-Automata Format,
in Proceedings of CAV 2015, volume 9206 of LNCS, pages 479-486. Springer-Verlag, 2015.
[DOI link,
preprint PDF,
format specification]
-
F. Blahoudek, A. Duret-Lutz, M. Křetínský, and J. Strejček:
Is There a Best Büchi Automaton for Explicit Model
Checking?,
in Proceedings of SPIN 2014, pages 68-76. ACM, 2014.
[DOI link,
preprint PDF,
corresponding data]
-
F. Blahoudek: Chasing the Best Büchi Automata for Nested Depth-first Search Based Model Checking.,
in Proceedings of MOVEP'14, 2014.
[PDF]
-
F. Blahoudek, M. Křetínský, and J. Strejček:
Comparison of LTL to Deterministic Rabin Automata
Translators, in Proceedings of LPAR 2013, volume 8312 of LNCS,
pages 164-172. Springer-Verlag, 2013.
[DOI link,
preprint PDF,
©
Springer-Verlag, LNCS]
-
T. Babiak, F. Blahoudek, M. Křetínský, and J. Strejček:
Effective Translation of LTL to Deterministic Rabin Automata:
Beyond the (F,G)-Fragment, in Proceedings of ATVA 2013, volume
8172 of LNCS, pages 24-39. Springer-Verlag, 2013.
[DOI link,
preprint PDF,
©
Springer-Verlag, LNCS,
full version on arXiv]