About me

My name is Jan Tušil. I have 9+ years in professional software engineering, split between embedded systems and formal methods. I also have a PhD in Computer Science from Faculty of Informatics, Masaryk University, Brno, Czech Republic. My professional interests are centered around applications of formal methods for software engineering, which enforce conceptual clarity of designs and code, and also around embedded systems. My publications are listed in dblp. In my free time, I produce music.

Origin story

When I was a kid, I was into music a lot. I once built a simple monophonic synthesizer of a PS/2 keyboard, a PWM-controlled speaker, and an Intel 8051-based development kit programmed in assembly; I also built a software-based simulator for the 8051 to assist me with debugging. Later, during my undergraduate studies focused on embedded systems, I had a side-job as an embedded systems programmer. I was using primarily C and C++, and developed an interest in various software tools that assist programmers with development - such as static analysis tools. To be honest, when I first heard about formal methods as a first-year undergraduate, I thought these were just lawyerish regulatory documents written in natural language; I completely ignored these until I discovered Frama-C while searching for C analyzers. But Frama-C’s deductive verification capabilities amazed me. Back then, there were no deductive verification tools for C++, so I wanted to build my own tool like that. Eventually, I joined a company that focused on such tools, and also pursued a PhD in formal methods. The interest in formal methods and embedded systems remained until today.

Further reading

• Why I got into formal methods? further details my embedded-to-formal story.
• Debugging by proof attempts? discusses my personal experience with parallels and tensions between proving, testing, and debugging.
• Computer data should represent real-world things, not abstract nonsense is a fable on the practical utility of abstractions.

Open to collaboration

I am open to discussions regarding research collaborations, postdoctoral positions, and consulting engagements. I am particularly interested in projects that require rigorous analysis and deep problem solving, where the ability to synthesize insights from scientific literature makes a practical difference - whether in formal methods, embedded systems, or research in algorithms and logic. Feel free to contact me at jan.tusil@proton.me.