Mukesh Tiwari

Welcome to my webpage. My name is Mukesh Tiwari, and currently, I am a Senior Research Fellow at the University of Cambridge and working on formal verification of networking protocols, from algebraic point of view, with Timothy Griffin. The goal is to extract a verified OCaml implementation that will help network-protocol designers to verify the properties of their protocol. Before joining the University of Cambridge, I was a research fellow at the University of Melbourne where I worked on formally verified information flow security with Toby Murray. Before moving to Melbourne, I was a PhD student at the Australian National University, Canberra where I worked on formal verification of electronic voting algorithms in Coq, under the supervision of Dirk Pattinson. You can read my thesis  (Coq source code).

My research focuses on proving the correctness of software programs, particularly used for a very high stake situations, e.g., vote counting software for a legally binding elections to a public office, data processing software for sensitive data, cryptographic software used in elections, etc. Mainly, I use Coq theorem prover to implement software programs and prove them correct. Feel free to get in touch if you have any research project related to theorem proving, particularly if it involves Coq.