CV

Timeline

• 2025–now: associate professor in the VeriFIT group at Faculty of Information Technology, Brno University of Technology, Czech Republic
• 2016–2025: assistant professor in the VeriFIT group at Faculty of Information Technology, Brno University of Technology, Czech Republic
• 2015–2016: postdoc with Yu-Fang Chen at Institute of Information Science, Academia Sinica, Taiwan, Republic of China
• 2010–2015: Ph.D. student under Tomáš Vojnar in the VeriFIT group at Faculty of Information Technology, Brno University of Technology, Czech Republic
• 2005–2010: Bc. and MSc. student at Faculty of Information Technology, Brno University of Technology, Czech Republic

Membership

• CAV’26 Artifact Evaluation co-chair (together with Magnus Myreen)
• VMCAI’26 PC co-chair (together with Yu-Fang Chen and Thomas Jensen)
• MOSCA’25 co-organiser (together with Joel Day and Matthew Hague)
• ESOP/FASE/FoSSaCS’25 Artifact Evaluation co-chair (together with Laura Bussi, Michalis Kokologiannakis, and Stefan Winter)
• AVM’19 co-organiser (together with Tomáš Vojnar and Jan Strejček)
• ATVA’19 Artifact Evaluation chair
• TACAS’19 Artifact Evaluation co-chair (together with Ernst Moritz Hahn)
• Program committees:
  • OOPSLA’27
  • VECoS’26
  • FMCAD’26
  • SMT’26
  • CAV’26
  • PAAR’26
  • PLDI’26
  • DATE’26
  • VECoS’25
  • VQC’25
  • CAV’25
  • SPIN’25
  • PhD-iFM’24
  • VECoS’24
  • FMCAD’24 Student Forum
  • PAAR’24
  • SPIN’24
  • DATE’24
  • PhD-iFM’23
  • VECoS’23
  • ATVA’23
  • APLAS’22
  • EXPRESS/SOS’22
  • VECoS’22
  • PAAR’22
  • VECoS’21
  • PAAR’20
  • VECoS’20
  • ATVA’20
  • ATVA’19
  • TACAS’18 Artifact Evaluation
  • RP’17
  • SV-COMP’16
  • SV-COMP’15
• 龍龖龘隊
• The fanclub of Ondra Lengál (link)

Awards

• SMT-COMP:
  • Z3-Noodler (solver for the theory of strings):
    • 2026: winner of the QF_Strings division (single query track) under all scoring schemes, as well as the categories for the logics QF_S and QF_SLIA.
    • 2025: together with a derived solver based on it, getting the first two places in the QF_Strings division (single query track) under all scoring schemes, as well as the categories for the logics QF_S and QF_SLIA.
    • 2024: winner of the QF_Strings division (single query track) under all scoring schemes, as well as the categories for the logics QF_S and QF_SLIA.
  • Amaya (solver for the linear integer arithmetic):
    • 2026: overall winner of the largest contribution (single query) category (under sequential and parallel scoring schemes) and winner of the LIA logic (single query) category under the sat scoring scheme.
    • 2025: third place in the LIA logic (single query) category under the sequential and parallel performance scoring schemes and the second place in the NIA logic under the UNSAT performance scoring scheme.
    • 2024: winning the NIA logic (single query) category under the 24s performance scoring scheme (and second palce under the sequential performance, parallel performance, and UNSAT performance scoring schemes, and the third place under the SAT performance scoring scheme).
• Our PLDI’23 paper An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits was chosen as a CACM Research Highlight.
• A Distinguished paper award for the paper Solving String Constraints with Lengths by Stabilization at OOPSLA’23.
• A Distinguished paper award for the paper An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits at PLDI’23.
• A Best paper award for the paper Word Equations in Synergy with Regular Constraints at FM’23.
• A Best paper award for the paper Automata Terms in a Lazy WSkS Decision Procedure at CADE-27 (2019).
• Prize of Antonín Svoboda for the best PhD thesis in Computer Science (Czech Republic, 2016)
• A co-authored separation logic solver SPEN won the division qf_shlid_ent of international Competition of Solvers for Separation Logic (SL-COMP) 2014 and was the second in divisions qf_shls_entl and qf_shls_sat in both SL-COMP 2014 and SL-COMP 2018.
• First place at MSc Thesis of the Year competition (Czech Republic, 2010)
• Dean’s prize for MSc thesis (FIT BUT, 2010)
• Prize of Zdena Rábová (a prize for exceptional students at FIT BUT, 2009)
• Two first place awards at a local student research competition (EEICT 2008, EEICT 2010)
• GE Foundation Scholar-Leaders scholarship (Czech Republic, 2007)

Links

• Google Scholar
• DBLP
• ORCID
• Scopus