Dr. Marek Košta

Researcher
Slovak Academy of Sciences
Institute of Informatics
Dúbravská cesta 9
845 07 Bratislava, Slovakia
Mail: marek.kosta@savba.sk
Phone: +421 2 5941 1279
PGP key: 23A08E95
Pre študentov:
Ponúkam široké spektrum tém (od praktických zahŕňajúcich implementáciu až po teoretické) záverečných prác (Bc., Ing., Mgr.) v oblastiach matematiky a informatiky. V prípade otázok a/alebo záujmu ma kontaktujte e-mailom.

Research Interests

My research lies on the boundary between symbolic computation, automated reasoning, and satisfiability checking. Currently I focus on real quantifier elimination, real decision procedures, and reasoning with real arithmetic constraints. Furthermore, I am interested in theories of integers, e.g., Presburger Arithmetic, and their applications.

I have been an active developer of the open-source computer logic system Redlog since 2012.

Projects

I am an external expert and associate of the ongoing project H2020-FETOPEN-2015-CSA_712689 SC-Square of the European Union.

Within the SMArT project funded by the ANR and DFG I worked on adaptation of state-of-the-art arithmetic decision procedures for use within an SMT context in order to support formal system verification.

Within the AVACS project funded by the DFG I worked on development and efficient applications of Cylindrical Algebraic Decomposition and Virtual Substitution in the context of non-linear real constraint solving.

Education

  • Ph.D. in Computer Science (summa cum laude) at the Saarland University and the Max Planck Institute for Informatics, 2016
  • M.Sc. in Computer Science (with honors) at the Comenius University, 2011

Awards

  • International Max Planck Research School Scholarship, 2011
  • Comenius University Rector's award for an outstanding Master's Thesis, 2011

Selected Publications

  • New Concepts for Real Quantifier Elimination by Virtual Substitution.
    Doctoral Dissertation, Saarland University, 2016.
  • Better Answers to Real Questions (with T. Sturm, A. Dolzmann).
    Journal of Symbolic Computation 74:255–275, 2016.
  • Constructing a Single Cell in Cylindrical Algebraic Decomposition (with C. Brown).
    Journal of Symbolic Computation 70:14–48, 2015.
  • Towards Conflict-Driven Learning for Virtual Substitution (with K. Korovin, T. Sturm).
    CASC 2014, LNCS 8660, pp.256–270, 2014.
  • SMT-Based Compiler Support for Memory Access Optimization for Data-Parallel Languages.
    Proceedings of the 5th International Conference on Mathematical Aspects of Computer and System Sciences (MACIS), pp.36–42, 2013.
  • Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages (with R. Karrenberg, T. Sturm).
    FroCoS 2013, LNAI 8152, pp.56–70, 2013.
full list of publications

Academic Activities

  • Publicity Chair at MACIS 2013
  • Reviewer for Journal of Symbolic Computation and Mathematics in Computer Science
  • Reviewer at conferences ADG, CASC, ISSAC, LPAR