Henrich Lauko is a PhD candidate at the Faculty of Informatics, Masaryk University in Brno. He is intrigued by both theoretical and engineering aspects of computer science. He finds the sweet spot for both in program verification, where he focuses on the development of reusable analyses using compiler toolchains.