Mohammad Hossein Khoshechin Jorshari

Hello, visitor! I’m Mohammad (you can also call me KC), a PhD student in the Rigorous Software Engineering group at the Max Planck Institute for Software Systems (MPI-SWS) in Germany, supervised by Rupak Majumdar. My main research focus is on the automated systematic verification of concurrent and distributed software, using dynamic partial order reduction and symbolic execution techniques. In tandem with my theoretical work on software verification, I also develop practical tools for software model checking. In particular, I am a core developer of the Java Model Checker (JMC), a stateless model checker designed for verifying and testing concurrent and distributed Java programs. If you are interested in doing a bachelor’s or master’s thesis, practical work, or internship over the topics of JMC, please check out the student projects page for more information.

My current research interests encompass formal verification, model checking, concurrency theory, the theory of distributed systems, automata theory, temporal logic, and database theory. If you are interested in these topics and would like to chat, please feel free to reach out!

Before joining MPI-SWS, I completed my Master’s degree in Computer Engineering at the Sharif University of Technology in Iran, where I worked on the specification and verification of timed distributed systems under the supervision of Ali Movaghar and Marjan Sirjani. I also hold a Bachelor’s degree in Computer Engineering from the Azad University, South Tehran Branch in Iran, where I worked on the theory of non-first normal form (NF2) databases under the supervision of Amir Hossein Rouhani Seraji.