I have now moved to Vienna. Please find my current webpage here.

I am a Research Associate in First-Order Theorem Proving and Verification in the Formal Methods Group in the School of Computer Science at the University of Manchester.

Previously, I was a Ph.D. student at 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.

- Automated reasoning
- Linear temporal logic and symbolic reachability analysis
- Hardware verification
- Automated planning

I am one of the developers of the automated theorem prover Vampire.

My past project include:

- Property Directed Reachability for Automated Planning
- Triggered Clause Pushing for IC3
- Duality in STRIPS planning
- Variable and Clause Elimination for LTL
- LS4: A PLTL-prover based on labelled superposition with partial model guidance
- Labelled Superposition for PLTL
- SPASS-XDB

- Resolution-based Methods for Linear Temporal Reasoning (PhD dissertation)

defended in October 2015 - Variable and Clause Elimination for LTL Satisfiability Checking

Suda M., Mathematics in Computer Science, 9(3): 327-344 (2015) - Playing with AVATAR

Reger G., Suda M., Voronkov A., CADE 2015: 399-415 (2015) - Property Directed Reachability for Automated Planning

Suda M., J. Artif. Intell. Res. (JAIR), 50:265–319 (2014) - Variable and clause elimination for LTL satisfiability checking

Suda M., in MACIS 2013 Nanning, China (eds. M. Košta and T. Sturm), pp. 60–74. (2013) - A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance

Suda M., Weidenbach C., in IJCAR 2012 (eds. B. Gramlich, D. Miller, and U. Sattler), LNAI 7364, pp. 537-543. Springer, Heidelberg (2012) - Labelled Superposition for PLTL

Suda M., Weidenbach C., in LPAR-18 (eds. N. Björner and A. Voronkov), LNCS 7180, pp. 391-405. Springer, Heidelberg (2012) - On the Saturation of YAGO

Suda M., Weidenbach C., Wischnewski P., in 5th International Joint Conference on Automated Reasoning, IJCAR 2010 (eds. J. Giesl, R. Hähnle), LNCS 6173, pp. 441-456. Springer, Heidelberg (2010) - Progress Towards Effective Automated Reasoning with World Knowledge

G. Sutcliffe, M. Suda, A. Teyssandier, N. Dellis, G. de Melo, in Proceedings of the 23rd International FLAIRS Conference, AAAI Press, Menlo Park, CA, USA. (2010) - External Sources of Axioms in Automated Theorem Proving

M. Suda, G. Sutcliffe, P. Wischnewski, M. Lamotte-Schubert, G. de Melo, in Proceedings of the 32nd Annual Conference on Artificial Intelligence (eds. B. Mertsching), LNAI 5803, pp. 281-288. Springer, Heidelberg (2009) - SPASS Version 3.5

C. Weidenbach, D. Dimova, A. Fietzke, R. Kumar, M. Suda, and P. Wischnewski, in Automated Deduction - CADE-22 Proceedings (eds. R. A. Schmidt), LNCS (LNAI), vol. 5663, pp. 140-145. Springer, Heidelberg (2009) - Relevancy Zones for Lambda Search in Rigid Board Games

M. Suda, in WDS'08 Proceedings of Contributed Papers: Part I - Mathematics and Computer Sciences (eds. J. Safrankova and J. Pavlu), pp. 151-158. Matfyzpress , Prague (2008)

Room 2.46

Manchester, Greater Manchester, M13 9PL

United Kingdom

Last updated: 12. 4. 2016