Mikhail Starchak

Research Group Leader
Algorithms, Theory & Logic

My research focuses on the development of algorithms for arithmetic theories. This includes the computational complexity of decision procedures, characterisations of the expressive power, and optimizations that make algorithms for arithmetic theories applicable in the practice of SMT-solving. I am currently also involved in the Algorithmic Verification work package (PI: Prof. Joël Ouaknine) of the ERC-Synergy grant Dynamical and Arithmetical Model Checking — DynAMiCs.

I obtained my CSc. of physical and mathematical sciences (Ph.D.) degree at the Department of Mathematics and Computer Science of the Saint Petersburg State University. Prior to joining MPI-SWS, I was an Assistant Professor (2024-2025) and, previously, a Teaching Assistant (2017-2023) at the Saint Petersburg State University.

Office
Building E1 5, Room 454
Campus
Saarbrücken

Mailing address
Mikhail Starchak
Max Planck Institute for Software Systems
Campus E1 5
66123 Saarbrücken, Germany

Research

Research Interests

Arithmetic theories: expressivity, decidability, complexity, applications in SMT-solving

Publications

Quantifier Elimination for Regular Integer Linear-Exponential Programming

Proceedings of LICS 2025 [doi]
One-Parametric Presburger Arithmetic has Quantifier Elimination

with Alessio Mansutti

Proceedings of MFCS 2025 [doi] [arxiv]
Formal Languages and Arithmetic Theories: Recent Results and Open Problems

with Christoph Haase [Short survey]

Proceedings of DLT 2025 [doi]
Integer Linear-Exponential Programming in NP by Quantifier Elimination

with Dmitry Chistikov, and Alessio Mansutti

Proceedings of ICALP 2024 [Best ICALP Paper Track B] [doi] [arxiv]
Existential Definability of Unary Predicates in Büchi Arithmetic

Proceedings of CiE 2024 [doi]
Existential Arithmetics with Addition and Bitwise Minimum

Proceedings of FoSSaCS 2023 [doi]
Quasi-Quantifier Elimination Algorithms and Definability Problems in Arithmetics with Divisibility

PhD thesis, Saint Petersburg State University, 2022 [pdf]
Positive Existential Definability with Unit, Addition and Coprimeness

Proceedings of ISSAC 2021 [doi]
A Proof of Bel'tyukov-Lipshitz Theorem by Quasi-Quantifier Elimination

Vestnik St.Petersb. Univ.Math. (2021) (Part I: [doi]) (Part II: [doi])
Some Decidability and Definability Problems for the Predicate of Divisibility by Two Consecutive Integers

Comp.Tools Ed. (2018) (in Russian)

Software

Chrobelias - SMT-solver for Exp-Linear Integer Arithmetic and Strings

Funding

Existential Arithmetics with Addition and Regular Predicates
Russian Science Foundation (RSF) grant for young researchers (Project # 23-71-01041). 07.2023 - 06.2025.

Research

Research Interests

Publications

Software

Funding

Program committee member