Jasper Nalbach

Email

Address

Room 4228
Ahornstraße 55
D-52074 Aachen

Phone

+49 241 80 21246

I am a postdoctoral researcher at the Theory of Hybrid Systems group. Since November 2025, I am also a Collaborateur de l’Université de Liège. Previously, I did my PhD at the Theory of Hybrid Systems group under the supervision of Erika Ábrahám and was an associate member of the UnRAVeL training group from April 2020 to November 2025.

My website contains a list of publications and talks, including preprints and slides. See also ORCID and dblp.

Research interests

My primary research interest lies in real algebraic methods for SMT solving, with a particular emphasis on cylindrical algebraic decomposition (CAD). Additionally, I am exploring incomplete methods and their integration with CAD-based algorithms to address real-world problems more efficiently.

In my PhD thesis, I adapted and enhanced exploration-guided algorithms – specifically NLSAT, cylindrical algebraic coverings (CAlC), and non-uniform CAD (NuCAD). These algorithms build upon CAD while minimizing computational effort for tasks such as satisfiability checking and quantifier elimination. Furthermore, I developed a proof system for these algorithms that captures their common operations while allowing for fine-grained improvements based on underlying CAD theory. This system also facilitates the generation of certificates for unsatisfiability results. Together with my collaborators, we introduced novel notions that contribute to the theory underpinning the CAD. All algorithms have been implemented in the open-source SMT solver SMT-RAT, which is currently leading in the SMT-COMP division for non-linear real arithmetic involving quantifiers.

Teaching

• Lecture: Satisfiability Checking (WS20/21, WS21/22, WS22/23, WS23/24, WS24/25, WS25/26, WS26/27)
• Lecture: Algorithmen und Datenstrukturen (Service) (SS20, SS22)
• Lecture: Hybrid Systems (SS21)
• Seminar: Formal Methods (WS26/27)
• Seminar: Satisfiability Checking (SS20, WS20/21, SS21, WS21/22, SS22, SS23, SS25, SS26)
• Proseminar: Formal Methods (WS20/21, SS21, WS21/22)
• Practical Lab: Neural Network Verification with Reluplex (WS20/21)

Student theses

In progress

• Carsten Perkampus, “Formalizing a proof system for single cell construction in lean” (Master thesis, supervision Erika Ábrahám, Jasper Nalbach, Valentin Promies)

Completed

• Jan Bienmüller, “Abstraction techniques in exploration-guided algorithms for real algebra” (Bachelor thesis 07/2025, supervision Erika Ábrahám, Valentin Promies, Jasper Nalbach)
• Alexej Kolbin, “Traversal heuristics for cylindrical algebraic coverings” (Bachelor thesis 02/2025, supervision Erika Ábrahám, Jasper Nalbach)
• Carsten Perkampus, “Speed up single cell construction via combinatorial optimization” (Bachelor thesis 04/2024, supervision Erika Ábrahám, Jasper Nalbach)
• Philip Kroll, “Implementation of cylindrical algebraic coverings for quantifier elimination” (Master thesis 12/2023, supervision Erika Ábrahám, Jasper Nalbach)
• Paul Tristan Wagner, “Piecewise linear under-approximation of cell boundaries in MCSAT” (Bachelor thesis 07/2023, supervision Erika Ábrahám, Jasper Nalbach)
• Philippe Specht, “Improving incremental linearization for satisfiability modulo non-linear real arithmetic checking” (Master thesis 04/2023, supervision Erika Ábrahám, Jasper Nalbach)
• Jonas Spang, “On the mechanisms of simplex heuristics” (Bachelor thesis 08/2022, supervision Erika Ábrahám, Jasper Nalbach)
• Max Harder, “Generating coverings using virtual substitution for explanations in mcSAT” (Bachelor thesis 08/2022, supervision Erika Ábrahám, Jasper Nalbach)
• Philipp Bär, “Exploiting strict constraints in the computations of cylindrical algebraic coverings” (Bachelor thesis 08/2022, supervision Erika Ábrahám, Jasper Nalbach)
• Valentin Promies, “Underapproximating cell bounds in MCSAT using low-degree polynomials” (Master thesis 08/2022, supervision Erika Ábrahám, Jasper Nalbach)
• Svenja Stein, “An incremental adaption of the FMPlex method for solving linear real algebraic formulas” (Bachelor thesis 05/2022, supervision Erika Ábrahám, Jasper Nalbach)
• Kai Hilgers, “An FMplex-inspired simplex heuristics” (Bachelor thesis 03/2022, supervision Erika Ábrahám, Jasper Nalbach)
• André Poncelet, “Conflict generalization for quadratic real-arithmetic constraints in SMT-RAT” (Bachelor thesis 12/2021, supervision Erika Ábrahám, Jasper Nalbach)
• Boris Schüpp, “Quantifier elimination using the virtual substitution” (Bachelor thesis 09/2021, supervision Erika Ábrahám, Jasper Nalbach)
• Paul Kobialka, “Connecting simplex and Fourier-Motzkin into a novel quantifier elimination method for linear real algebra” (Master thesis 07/2021, supervision Erika Ábrahám, Jasper Nalbach)
• Thomas Bauer, “Quantifier elimination for real-arithmetic problems with Boolean structure using the Fourier-Motzkin method” (Bachelor thesis 2021, supervision Erika Ábrahám, Jasper Nalbach)
• Daniel Heinen, “Purging spurious samples in the cylindrical algebraic decomposition” (Bachelor thesis 11/2020, supervision Erika Ábrahám, Jasper Nalbach)
• Fabian Alieff, “Simplex heuristics in SMT solving” (Bachelor thesis 11/2020, supervision Erika Ábrahám, Jasper Nalbach)
• Philip Kroll, “Efficient data structures for cylindrical algebraic coverings” (Bachelor thesis 10/2020, supervision Erika Ábrahám, Jasper Nalbach)
• Philippe Specht, “A level-wise variant of single cell construction in cylindrical algebraic decomposition” (Bachelor thesis 09/2020, supervision Erika Ábrahám, Jasper Nalbach)

Publications