I am the Satisfiability Modulo Theory (SMT) Team Lead at Certora. Certora is the leader in formal verification of Ethereum Smart Contracts and our Certora Verification Tool helps to secure hundreds of billions USDs held in Decentralised Financial Applications. My goal is to improve the scalability of our formal verification techniques, especially targeting the SMT part of our tool.

Before joining Certora, I was a Post-doctoral researcher at the Max-Planck Institute for Software Systems in Rupak Majumdar’s group. I also used to be a research fellow at the National University of Singapore, working with Kuldeep S. Meel and people from the MeelGroup. I received my Ph.D. at the Masaryk University in Czech Republic, supervised by Ivana Černá.

My research interests are at the intersection of formal methods and constraint processing. Especially, I focus on formal software verification and on analysis of infeasible constraint systems such as unsatisfiable Boolean formulae or inconsistent sets of software requirements.

Download my resumé.