Previous Experience
Martin Suda currently holds a senior researcher position at CIIRC CTU, conducting research in areas of Automated Reasoning (AR) and Machine Learning (ML). He’s a PI of the Czech Science Foundation project PowerATP and an investigator of RICAIP. Previously, he was a postdoc at the University of Manchester, UK and at TU Wien, Vienna, Austria focusing on Automated Theorem Proving.
He has received his Ph.D. from the Max-Planck-Institut für Informatik and the Saarland University in Saarbrücken, Germany, and at the Faculty of Mathematics and Physics, Charles University in Prague, Czech Republic.
Martin Suda is known as a co-developer of and one of the researchers behind Vampire, a world leading automatic theorem prover for first-order logic with theories, as exemplified by its victories at the annual CADE ATP System Competition and by its strong participation at SMTCOMP.
Current Focus
Martin Suda plans to pursue research where he can develop rigorous mathematical theories as foundations to building software with actual practical impact. In addition to Automated Reasoning his research interests include Theory of Boolean Satistiablity, QBF and DQBF solving, and Automated Planning.
Publications
| Bhayat, A., Suda, M. A Higher-Order Vampire (Short Paper) In: Benzmüller, C., Heule, M.J., Schmidt, R.A. (eds) Automated Reasoning. IJCAR 2024. Lecture Notes in Computer Science, vol 14739. Springer, Cham. | |
| Bártek, F., Chvalovský, K., Suda, M. Regularization in Spider-Style Strategy Discovery and Schedule Construction. In: Benzmüller, C., Heule, M.J., Schmidt, R.A. (eds) Automated Reasoning. IJCAR 2024. Lecture Notes in Computer Science(), vol 14739. Springer, Cham. | |
| Einarsdóttir, S.H., Hajdu, M., Johansson, M., Smallbone, N., Suda, M. Lemma Discovery and Strategies for Automated Induction. In: Benzmüller, C., Heule, M.J., Schmidt, R.A. (eds) Automated Reasoning. IJCAR 2024. Lecture Notes in Computer Science(), vol 14739. Springer, Cham. | |
| Filip Bártek, Karel Chvalovský, Martin Suda Cautious Specialization of Strategy Schedules PAAR’24: 9th Workshop on Practical Aspects of Automated Reasoning. CEUR Workshop proceedings | |
| Jan Jakubuv, Karel Chvalovský, Zarathustra Amadeus Goertzel, Cezary Kaliszyk, Mirek Olsák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, Josef Urban MizAR 60 for Mizar 50, Fourteenth Conference on Interactive Theorem Proving – ITP, 2023 | |
| Jan Jakubuv, Karel Chvalovský, Zarathustra Amadeus Goertzel, Cezary Kaliszyk, Mirek Olsák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, Josef Urban MizAR 60 for Mizar 50, Fourteenth Conference on Interactive Theorem Proving – ITP, 2023 | |
| Filip Bártek, Martin Suda How Much Should This Symbol Weigh? A GNN-Advised Clause Selection, 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning – LPAR , 2023 | |
| Michael Rawson, Martin Suda, Petra Hozzová, Giles Reger: Reuse of Introduced Symbols in Automatic Theorem Provers. PAAR’22: 8th Workshop on Practical Aspects of Automated Reasoning, August 11–12, 2022. | |
| M Suda: Vampire Getting Noisy: Will Random Bits Help Conquer Chaos? (System Description). IJCAR 2022: 659-667 Lecture Notes in Computer Science(), vol 13385. Springer, Cham. DOI 10.1007/978-3-031-10769-6_38 | |
| M Suda: Improving ENIGMA-style Clause Selection while Learning From History. In: Automated Deduction – CADE 28. 28th International Conference on Automated Deduction, Pittsburgh, 2021-07-12/2021-07-15. Springer, Cham, 2021. p. 543-561. Lecture Notes in Artificial Intelligence. vol. 12699. ISSN 0302-9743. ISBN 978-3-030-79875-8. DOI 10.1007/978-3-030-79876-5_31 | |
| F Bártek, M Suda: Neural Precedence Recommender. In: Automated Deduction – CADE 28. 28th International Conference on Automated Deduction, Pittsburgh, 2021-07-12/2021-07-15. Springer, Cham, p. 525-542. Lecture Notes in Artificial Intelligence. vol. 12699. ISSN 1611-3349. ISBN 978-3-030-79876-5. DOI 10.1007/978-3-030-79876-5_30 | |
| N Froleyks, M Heule, M Iser, M Järvisalo, M Suda: SAT Competition 2020. Artificial Intelligence. 2021, 301 ISSN 0004-3702. DOI 10.1016/j.artint.2021.103572 | |
| M Suda: Vampire with a Brain Is a Good ITP Hammer. In: Frontiers of Combining Systems. 13th International Symposium, FroCoS 2021, Birmingham, 2021-09-08/2021-09-10. Cham: Springer, 2021. p. 192-209. 1. ISSN 0302-9743. ISBN 978-3-030-86204-6. DOI 10.1007/978-3-030-86205-3_11 |