CV

Timeline

• 2016–now: 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 and Lukáš Holík 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

• FoSSaCS’25 Artifact Evaluation chair
• 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:
  • 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

• A co-authored string solver Z3-Noodler won the QF_Strings division (single query track) of SMT-COMP’24 under all scoring schemes, as well as the categories for the logics QF_S and QF_SLIA
• A co-authored linear integer arithmetic (LIA) solver Amaya won the NIA logic (single query) category of SMT-COMP’24 under the 24s performance scoring scheme (and was the second under the sequential performance, parallel performance, and UNSAT performance scoring schemes, and the third under the SAT performance scoring scheme)
• 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