Henrich is a PhD candidate at the Faculty of Informatics, Masaryk University in Brno, supervised by Jiří Barnat. Red Hat Czech supports his research efforts.
The focus of his research is on analysis and verification of C/C++ programs. Currently, Henrich is mostly interested in the efficient representation of program inputs (nondeterministic data) for the verification.
He mainly concentrates on how to adapt existing techniques like symbolic execution or abstract interpretation to a general framework LART – LLVM Abstraction and Refinement Tool. This framework leverages program instrumentationand allows to design input data representation easily.
Furthermore, he engages in the teaching of courses, especially algorithms and data structures, introduction to programming and parallel programming.