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