Martin Suda

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.

Research interests

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

Projects

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

Publications

• 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)

Contact Information

Last updated: 12. 4. 2016