Mikoláš Janota
RICAIP Tenure Track holder
Head of the Formal Methods Research Group at the Czech Institute of Informatics, Robotics and Cybernetics (CIIRC)
Formal Methods – Automated Reasoning – SAT Solving
Previous Experience
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.
Current Focus
Mikoláš has been working on the development of Formal Methods and Automated Reasoning during his whole academic career spanning now over 16 years, which includes SW verification, SAT, MaxSAT, or SMT solvers. Mikoláš Janota’s main focus is the advancement of Satisfiability Modulo Theories solvers in general. The concrete applications of the technology span from computational algebra to scheduling problems. He collaborates with the Prague testbed team in the form of consultations regarding the topics of scheduling and formal reasoning. He is contributing to the development of the SMT cvc5, and more recently, has been applying machine learning to improve SAT based solvers. He is the head of the Formal Methods Research Group at the Czech Institute of Informatics, Robotics and Cybernetics (CIIRC). He is the Principal Investigator and main beneficiary in the POSTMAN project (ERC CZ, 2020-2025) and is involved in the ROBOPROX project within the Czech Programme Johanes Amos Comenius.
Recent successes and results – What recent research achievements or milestones are you most proud of?
Probably the biggest milestone was completing the ERC-CZ project POSTMAN, which focused on applying machine learning to SMT solvers. The project ran from January 2020 to December 2025 with a budget of 2.5 million EUR and received an Excellent final evaluation (the highest possible rating). We demonstrated that neural networks can learn to select quantifier instantiations in the SMT solver cvc5, a result published in a journal in 2026. We also developed techniques for program repair that combine zero-shot learning with MaxSAT-based fault localization, published at AAAI 2025. On the combinatorial side, our work on SAT-based finite model finding, including symmetry breaking and lexicographically smallest models, led to a Best Paper Award at CICM 2024. I was also invited to give a tutorial on synthesis in SMT at Dagstuhl Seminar 25231 in 2025.
Biggest challenges and future plans – What are the main challenges currently facing your research areas, and what directions do you plan to pursue in the coming years?
Modern SAT and SMT solvers are very powerful but rely on hand-crafted heuristics that are difficult to improve systematically. The key open problem is how to learn better heuristics, ones that work across problem families rather than just on specific benchmarks. Scalability is a related issue: real-world verification tasks still push current tools to their limits.
In the coming years I plan to work on two fronts. First, using LLM-based agentic workflows to help construct and evaluate new reasoning algorithms, so that ideas from the literature can be implemented and tested with less manual effort. Second, distilling knowledge from large models into lightweight, locally deployable open-weight models fine-tuned for specific sub-tasks, removing dependence on external services at inference time. The goal is self-contained, high-quality automated reasoning that does not depend on proprietary infrastructure.
International collaborations with other teams/ projects etc. – Your work involves collaborations across institutions and projects. How do international partnerships influence your research, and what value do they bring?
International collaboration is central to my work. My research career has taken me through Ireland (PhD at University College Dublin), Portugal (INESC-ID Lisbon and Universidade de Lisboa), the UK (Microsoft Research Cambridge), and now Czechia (CIIRC, CTU Prague), and I have maintained strong ties with colleagues at each of these institutions.
My closest ongoing collaborators include Vasco Manquinho and Pedro Orvalho at IST Lisbon, with whom I work on MaxSAT and program repair. My work on finite model finding and computational algebra grew out of a collaboration with João Araújo (NOVA Lisbon), Michael Codish (Ben-Gurion University), and Petr Vojtěchovský (University of Denver). I also collaborate with Stefan Szeider and Markus Kirchweger at TU Wien on symmetry breaking and quantified graph search.
Beyond individual collaborations, I benefit from larger projects: as group leader in the ROBOPROX project, I coordinate formal-methods research objectives that require cross-disciplinary and cross-institutional work. Working with international partners exposes me to different problem domains and benchmarks, and has driven our group to apply SAT/QBF/SMT techniques to a wider range of areas, from program verification to computational algebra.
Tenure track position – How has progressing into a tenure-track research role influenced your career, both professionally and personally?
Obtaining a stable senior research position at CIIRC after years of post-doctoral and fixed-term appointments gave me the freedom to pursue longer-horizon projects, ones that take several years to pay off. POSTMAN is a direct example: building a research group, mentoring PhD students, and maintaining a focused agenda over six years would not have been feasible otherwise.
Professionally, the position brought leadership responsibilities: I now head the Formal Methods Group at CIIRC and since 2025 serve as Head of the Department of Artificial Intelligence. These roles push me to think about the group rather than just my own projects, which I find genuinely valuable. Personally, the stability allowed me to commit to Prague, invest in the local scientific community, and co-organize international events here (FMCAD 2024 in Prague).
Selected publications
| M. Janota, M. Olšák LLM2SMT: Building an SMT Solver with Zero Human-Written Code arxiv | |
| J. Araújo, F. M. Ferreira, M. Janota and M. Kinyon Forbidden substructure theorems: A computational tool applied to varieties of lazy magmas Mathematics of Computation (SJR) | |
| J. Jakubův, M. Janota, J. Piepenbrock, and J. Urban Machine learning for quantifier selection in cvc5 International Journal of Approximate Reasoning | |
| P. Orvalho, M. Janota, V. Manquinho MENTOR: Fixing Introductory Programming Assignments With Formula-Based Fault Localization and LLM-Driven Program Repair Journal of Systems and Software | |
| P. Orvalho, M. Janota, V. Manquinho InvAASTCluster: On Applying Invariant-Based Program Clustering to Introductory Programming Assignments Journal of Systems and Software | |
| D. Mojžíšek, J. Hůla, J. Janeček, D. Herel, M. Janota Geometric Reasoning in the Embedding Space Machine Learning and Knowledge Extraction | |
| M. Janota Experimental Results for Vampire on the Equational Theories Project arxiv | |
| M. Dančo, P. Hozzová, M. Janota From MBQI to Enumerative Instantiation and Back SMT Workshop 2025 | |
| Jan Jakubův, M. Janota Quantifier Instantiations: To Mimic or To Revolt? SMT Workshop 2025 | |
| C. E. Brown, K. Chvalovský, M. Janota, M. Olšák, S. Ratschan SMT and Functional Equation Solving over the Reals: Challenges from the IMO CADE 2025 | |
| J. Jakubův, M. Janota, and J. Urban Solving Hard Mizar Problems with Instantiation and Strategy Invention Conference on Intelligent Computer Mathematics 2024 (Best Paper Award) | |
| M. Janota, C. Chow, J. Araújo, M. Codish, P. Vojtěchovský SAT-based Techniques for Lexicographically Smallest Finite Models AAAI 2024 | |
| P. Orvalho, M. Janota, and V. Manquinho GitSEED: A Git-backed Automated Assessment Tool for Software Engineering SIGCSE Virtual 2024 | |
| P. Orvalho, M. Janota, and V. Manquinho CFaults: Model-Based Diagnosis for Fault Localization in C with Multiple Test Cases Formal Methods 2024 | |
| P. Orvalho, M. Janota, and V. Manquinho C-Pack of IPAs: A C90 Program Benchmark of Introductory Programming Assignments APR ’24: 5th ACM/IEEE International Workshop on Automated Program Repair | |
| C. E. Brown, M. Janota, M. Olšák Symbolic Computation for All the Fun Satisfiability Checking and Symbolic Computation, SC2 2024 | |
| J. Jakubův, M. Janota, J. Piepenbrock, and J. Urban Machine Learning for Quantifier Selection in cvc5 ECAI 2024 | |
| J. Araújo, C. Chow, M. Janota Symmetries for Cube-and-conquer in Finite Model Finding CP 2023 | |
| J. Jakubův, M. Janota, B. Piotrowski, J. Piepenbrock, and A. Reynolds Selecting Quantifiers for Instantiation in SMT SMT 2023 | |
| N. Antonov, P. Šůcha, and M. Janota Data-driven Single Machine Scheduling Minimizing Weighted Number of Tardy Jobs EPIA 2023 | |
| M. Janota, B. Piotrowski, K. Chvalovský Towards Learning Infinite SMT Models SYNASC 2023 | |
| P. Orvalho, J. Piepenbrock, M. Janota, V. Manquinho Graph Neural Networks For Mapping Variables Between Programs, ECAI 2023 | |
| J. Hůla, D. Adamczyk, M. Janota: Fast Heuristic for Ricochet Robots, In: Proceedings of the ICAART-23, 2023 | |
| M. Janota, A. Morgado, P. Vojtěchovský: Computing Generating Sets of Minimal Size in Finite Algebras, Journal of Symbolic Computation, 2023 | |
| C. E. Brown, M. Janota, and C. Kaliszyk: Challenges and Solutions for Higher-Order SMT Proofs, In: Proceedings of the 20TH SMT, 2022 | |
| M. Janota, J. Piepenbrock, B. Piotrowski: Towards Learning Quantifier Instantiation in SMT, In: Proceedings of the 25th SAT International Conference on Theory and Applications of Satisfiability Testing, 2022. | |
| F. Marques, A. Morgado, J. Fragoso Santos, M. Janota: TestSelector: Automatic Test Suite Selection for Student Projects,In: Proceedings of the 22nd International Conference on Runtime Verification, 2022 | |
| J. Hůla, J. Jakubův, M. Janota, and L. Kubej: Targeted Configuration of an SMT Solver, In: Proceedings of the 15TH CICM Conferences on Intelligent Computer Mathematics 2022, 2022 | |
| J. Araújo, C. Chow, M. Janota: Boosting Isomorphic Model Filtering with Invariants, CONSTRAINTS, 2022 | |
| M. Cabral, M. Janota, and V. Manquinho: SAT-based Leximax Optimisation Algorithms, In: Proceedings of the 25th SAT International Conference on Theory and Applications of Satisfiability Testing, 2022. | |
| M. Cabral, M. Janota, and V. Manquinho: How to Approximate Leximax-optimal Solutions, In: Proceedings of the 12th POS, 2021. | |
| C E Brown, M Janota: First-Order Instantiation using Discriminating Terms. In: Proceedings of the 19th International Workshop on Satisfiability Modulo Theories co-located with 33rd International Conference on Computer Aided Verification(CAV 2021). 19th International Workshop on Satisfiability Modulo Theories, Los Angeles, 2021-07-18/2021-07-19. Aachen: CEUR Workshop Proceedings, 2021. p. 17-22. vol. 2908. ISSN 1613-0073. | |
| J Jakubův, M Janota, A Reynolds: Characteristic Subsets of SMT-LIB Benchmarks. In: Proceedings of the 19th International Workshop on Satisfiability Modulo Theories co-located with 33rd International Conference on Computer Aided Verification(CAV 2021). 19th International Workshop on Satisfiability Modulo Theories, Los Angeles, 2021-07-18/2021-07-19. Aachen: CEUR Workshop Proceedings, 2021. p. 53-63. vol. 2908. ISSN 1613-0073. | |
| J Hůla, D Mojžíšek, M Janota: Graph Neural Networks for Scheduling of SMT Solvers. In: 2021 IEEE 33rd International Conference on Tools with Artificial Intelligence (ICTAI). The 33rd IEEE International Conference on Tools with Artificial Intelligence, Washington, 2021-11-01/2021-11-03. Los Alamitos: IEEE Computer Society, 2021. p. 447-451. ISSN 2375-0197. ISBN 978-1-6654-0898-1. DOI 10.1109/ICTAI52525.2021.00072 | |
| M Janota, A Morgado, J S Fragoso, V Manquinho: The Seesaw Algorithm: Function Optimization Using Implicit Hitting Sets. In: 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). The 27th International Conference on Principles and Practice of Constraint Programming, Montpellier, 2021-10-25/2021-10-29. Saarbrücken: Dagstuhl Publishing,, 2021. p. 1-16. vol. 210. ISSN 1868-8969. ISBN 978-3-95977-211-2. DOI 10.4230/LIPIcs.CP.2021.31 | |
| J Araújo, Ch Chow, M Janota: Filtering Isomorphic Models by Invariants. In: 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). The 27th International Conference on Principles and Practice of Constraint Programming, Montpellier, 2021-10-25/2021-10-29. Saarbrücken: Dagstuhl Publishing,, 2021. p. 1-9. vol. 210. ISSN 1868-8969. ISBN 978-3-95977-211-2. DOI 10.4230/LIPIcs.CP.2021.4 | |
| M Janota, et al.: Fair and Adventurous Enumeration of Quantifier Instantiations. In: Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021. 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021, Yale, 2021-10-20/2021-10-22. Wien: TU Wien, 2021. p. 256-260. Conference Series: Formal Methods in Computer-Aided Design. ISBN 978-3-85448-046-4. DOI 10.34727/2021/isbn.978-3-85448-046-4_35 |