Mikolas Janota graduated from Charles University in Prague, and got his doctoral degree from the University College Dublin. He held post doc positions at INESC-ID Portugal, and Cambridge, UK.
Throughout his academic career he has been interested in the practical applications of logic and automated reasoning, especially in the context of software development and verification. He has actively worked on the development of the verification tool ESC/Java and the application of satisfiability (SAT) solvers for product configuration (logic-based recommendation system). Also, he has focused on algorithms for Boolean logic, e.g. maximum satisfiability, minimum unsatisfiability, or quantified Boolean formula (QBF). His QBF solvers were the winner for several tracks of the recent QBF competitions. At Microsoft Research, Cambridge, UK he has actively participated on the development of the Microsoft SMT solver Z3.
Mikolas Janota is planning to build a research team at CIIRC CTU in the area of automated reasoning in combination with machine learning with the focus on software verification and other high-impact domains.