My name is Jan Tušil. Currently, I am a PhD student at Faculty of Informatics, Masaryk University, Brno, Czech Republic. My professional interests are centered around applications of formal methods for software engineering; I am also interested in embedded systems. My research so far was about language-parameteric program logics (such as Cartesian Reachability Logic) and related tools. I am using the Coq proof assistant for both research and personal projects, and C++ and Python for more pratically-oriented projects. Previously, my Master’s thesis was about formally modeling parts of the C++ language in K framework. My publications are listed in dblp. In my free time, I do some music.