I am a Ph.D. candidate at the Faculty of Informatics, Masaryk University in Brno. The focus of my research is on the analysis and the verification of C/C++ programs. Presently, I am mostly interested in the efficient representation of program inputs (nondeterministic data) for verification. I mainly focus on adapting existing techniques like symbolic execution or abstract interpretation to a general framework LART – LLVM Abstraction and Refinement Tool. This framework leverages program instrumentation and compiler tooling, allowing to design input data representation easily.


I engage in teaching at university, especially in courses on:

  • PB161 C++ programming,
  • IB002 algorithms and data structures,
  • IB111 foundations of programming,
  • IB102 automata and grammars,
  • PB152 operating systems,
  • IV112 parallel programming.

I am a co-author of exercise books for courses on algorithms and data structures and foundations of programming.


I actively engage in volunteering activities for high school students and puzzlehunt competitions. As a member of the Nordic Animals Association (IT student association that organizes events for high school students), I participate in the organization of:

  • KSI, a yearlong online seminar on computer science for high school students,
  • K-SCUK, a weeklong camp for students interested in computer science and/or biology,
  • InterLos, InterSob – puzzlehunt-like competitions.


  • SV-COMP 2019 – 2021 jury member of software verification competition

Personal website of Henrich Lauko