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
He 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. He is also contributing to the development of the SMT cvc5, and more recently, has been applying machine learning to improve SAT based solvers, mainly SMT (satisfiability modulo theories).
He is the head of the Formal Methods Research Group at the Czech Institute of of Informatics, Robotics and Cybernetics (CIIRC).
Publications
| 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 | |
| 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, 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 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 | |
| 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. | |
| 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. | |
| M. Cabral, M. Janota, and V. Manquinho: How to Approximate Leximax-optimal Solutions, In: Proceedings of the 12th POS, 2021. | |
| 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. | |
| 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, A. Morgado, P. Vojtěchovský: Computing Generating Sets of Minimal Size in Finite Algebras, Journal of Symbolic Computation, 2023 | |
| J. Hůla, D. Adamczyk, M. Janota: Fast Heuristic for Ricochet Robots, In: Proceedings of the ICAART-23, 2023 | |
| P. Orvalho, J. Piepenbrock, M. Janota, V. Manquinho Graph Neural Networks For Mapping Variables Between Programs, ECAI 2023 |