Modern satisfiability modulo theories (SMT) solvers are powerful engines that enable tackling challenging problems formulated in mathematical logic. However, their development is often driven by annual competitions while concrete applications are neglected. The project aims at making the solvers more accessible to everyday users and improve their efficiency on particular problems. Such problems may come from formal verification, smart contract verification, or formalized mathematics. Next-generation solvers should adapt to problems at hand, learn from previous successes, and try different approaches when failing.

We are seeking a highly motivated PhD candidate with a Master's degree in Computer Science, engineering, or a related field with an interest in applying mathematical logic, automated reasoning, and in particular, satisfiability modulo theories (SMT). 

The candidate is expected to contribute to international scientific research with excellent outcomes. This will require independent and innovative thinking and the ability to learn about new topics. The candidate is required to have excellent communication and writing skills in English and have substantial experience with code development.

We offer the opportunity to do scientifically challenging research on a fully funded position (1-year contract with the possibility of an extension of up to 4 years), including full social and health insurance. The research will be carried out at the​ Czech Institute of Informatics, Robotics, and Cybernetics (CIIRC) at the Czech Technical University in Prague. The institute was founded in 2013 and an important part of its mission is interdisciplinary cooperation, technology transfer, and collaboration with advanced industry. Among others, the institute hosts internationally renowned researchers ​R. Babuska (robotics), ​ Z. Hanzalek (scheduling and optimization), ​ V. Hlavac (vision, robotics), ​ V. Kucera (systems and control), ​ L. Lhotska (AI, biomedical engineering, human-machine interaction), ​ T. Mikolov (AI, learning), ​ T. Pajdla (vision, robotics, geometry), ​ J. Sedivy (NLP, learning), ​ J. Sivic (vision, learning), ​ O. Stepankova (biomedical engineering), ​ J. Urban (AI, reasoning).

Prague ranks among the top cities to live in (cf. Time Out Magazine index for 2022). The Dejvice Campus features a range of student amenities, such as the National Library of Technology, and a laid-back atmosphere with cafes and other social hangout places. Other benefits include a competitive salary, 30 days paid leave, and a family-friendly environment (Children’s corner, kindergarten, and elementary school operated by the Czech Technical University in Prague).