Mikoláš Janota

Mikoláš Janota

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

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. 


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
PDF
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
PDF
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
PDF
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
PDF
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.
PDF
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.
PDF