My name is Jan Tušil. I have a PhD in Computer Science from Faculty of Informatics, Masaryk University, Brno, Czech Republic; see also my university profile page. My professional interests are centered around applications of formal methods for software engineering; I am also interested in embedded systems. My research lies at the intersection of programming language theory and formal verification; more concretely, it is centered around the notion of a “programming language semantics framework”. I am using the Coq proof assistant for research projects and Rust, OCaml, 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.