Jasper Nalbach

About Me
mail@jaspernalbach.de, LinkedIn, and GitHub

I am a doctoral student at the Theory of Hybrid Systems group, RWTH Aachen University under the supervision of Erika Ábrahám and an associate member of the UnRAVeL training group since April 2020. Since November 2025, I am also a Collaborateur de l’Université de Liège.


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.


Since 2016, I am running the first blog on mate ice teas, called Der Mate-Connaisseur. Since 2019, I am active member of Uni.Urban.Mobil. e.V., a civil society organization for green transportation and urban development.

I support the TCS4F Manifesto.

Blog Posts
subscribe via RSS

Publications
ORCID, dblp, and Scopus

2025

  1. Jasper Nalbach, Lucas Michel, Erika Ábrahám, Christopher W. Brown, James H. Davenport, Matthew England, Pierre Mathonet, and Naïm Zénaïdi.
    Projective Delineability for Single Cell Construction
    2025.
    doi:10.48550/arXiv.2508.00512 (Preprint)
  2. Jasper Nalbach and Erika Ábrahám.
    A Variant of Non-uniform Cylindrical Algebraic Decomposition for Real Quantifier Elimination
    2025.
    doi:10.48550/arXiv.2508.00505 (Preprint)
  3. Valentin Promies, Jasper Nalbach, Erika Ábrahám, and Paul Kobialka.
    FMplex: Exploring a Bridge between Fourier-Motzkin and Simplex
    In Logical Methods in Computer Science. 2025.
    doi:10.46298/lmcs-21(2:6)2025 (Open Access)
    doi:10.5281/zenodo.7755862 (Artifact)
  4. Valentin Promies, Jasper Nalbach, and Erika Ábrahám.
    More is Less: Adding Polynomials for Faster Explanations in NLSAT [Best Paper Award @ CADE-30]
    In Automated Deduction (CADE-30). 2025.
    doi:10.1007/978-3-031-99984-0_7 (Open Access)
    doi:10.5281/zenodo.14916587 (Artifact)
    Preprint

2024

  1. Jasper Nalbach and Gereon Kremer.
    Extensions of the Cylindrical Algebraic Covering Method for Quantifiers
    2024.
    doi:10.48550/arXiv.2411.03070 (Preprint)
  2. Lucas Michel, Jasper Nalbach, Pierre Mathonet, Naïm Zénaïdi, Christopher W. Brown, Erika Ábrahám, James H. Davenport, and Matthew England.
    On Projective Delineability
    In Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2024). 2024.
    doi:10.1109/SYNASC65383.2024.00015
    doi:10.48550/arXiv.2411.13300 (Preprint w/o Copy Editing)
  3. Jasper Nalbach, Erika Ábrahám, Philippe Specht, Christopher W. Brown, James H. Davenport, and Matthew England.
    Levelwise construction of a single cylindrical algebraic cell
    In Journal of Symbolic Computation. 2024.
    doi:10.1016/j.jsc.2023.102288 (Open Access)
    doi:10.48550/arXiv.2212.09309 (Preprint w/ Appendix)
    doi:10.5281/zenodo.5764569 (Artifact)
  4. Jasper Nalbach and Erika Ábrahám.
    Merging Adjacent Cells During Single Cell Construction
    In Computer Algebra in Scientific Computing (CASC 2024). 2024.
    doi:10.1007/978-3-031-69070-9_15
    doi:10.5281/zenodo.11071146 (Artifact)
    Preprint w/o Copy Editing
  5. Valentin Promies, Jasper Nalbach, and Erika Ábrahám.
    Under-approximation of a single algebraic cell (extended abstract)
    In Satisfiability Checking and Symbolic Computation (SC-square 2024). 2024.
    https://ceur-ws.org/Vol-3717/short3.pdf (Open Access)

2023

  1. Jasper Nalbach, Valentin Promies, Erika Ábrahám, and Paul Kobialka.
    FMplex: A Novel Method for Solving Linear Real Arithmetic Problems
    In Games, Automata, Logics, and Formal Verification (GandALF 2023). 2023.
    doi:10.4204/EPTCS.390.2 (Open Access)
    doi:10.48550/arXiv.2309.03138 (Preprint w/ Appendix)
    doi:10.5281/zenodo.7755862 (Artifact)
  2. Erika Ábrahám, Jasper Nalbach, and Valentin Promies.
    Automated Exercise Generation for Satisfiability Checking
    In Formal Methods Teaching (FMTea 2023). 2023.
    doi:10.1007/978-3-031-27534-0_1
  3. Philipp Bär, Jasper Nalbach, Erika Ábrahám, and Christopher W. Brown.
    Exploiting Strict Constraints in the Cylindrical Algebraic Covering
    In Satisfiability Modulo Theories (SMT 2023). 2023.
    https://ceur-ws.org/Vol-3429/paper13.pdf (Open Access)
    doi:10.48550/arXiv.2306.16757 (Preprint w/ Appendix)
    doi:10.5281/zenodo.7900518 (Artifact)
  4. Gereon Kremer and Jasper Nalbach.
    Cylindrical Algebraic Coverings for Quantifiers
    In Satisfiability Checking and Symbolic Computation (SC-square 2022). 2023.
    https://ceur-ws.org/Vol-3458/paper1.pdf (Open Access)
  5. Jasper Nalbach and Erika Ábrahám.
    Subtropical Satisfiability for SMT Solving
    In NASA Formal Methods (NFM 2023). 2023.
    doi:10.1007/978-3-031-33170-1_26
    doi:10.5281/zenodo.7509171 (Artifact)
    Preprint

2021

  1. Jasper Nalbach, Erika Ábrahám, and Gereon Kremer.
    Extending the Fundamental Theorem of Linear Programming for Strict Inequalities
    In Symbolic and Algebraic Computation (ISSAC 2021). 2021.
    doi:10.1145/3452143.3465538
    Preprint

2020

  1. Jasper Nalbach.
    A novel adaption of the Simplex algorithm for linear real arithmetic
    Master's Thesis. 2020.
    doi:10.18154/RWTH-2021-04303 (Open Access)

2019

  1. Jasper Nalbach, Gereon Kremer, and Erika Ábrahám.
    On variable orderings in MCSAT for non-linear real arithmetic
    In Satisfiability Checking and Symbolic Computation (SC-square 2019). 2019.
    https://ceur-ws.org/Vol-2460/paper5.pdf (Open Access)

2017

  1. Erika Ábrahám, Jasper Nalbach, and Gereon Kremer.
    Embedding the Virtual Substitution Method in the Model Constructing Satisfiability Calculus Framework (work-in-progress paper)
    In Satisfiability Checking and Symbolic Computation (SC-square 2017). 2017.
    https://ceur-ws.org/Vol-1974/EAb.pdf (Open Access)
  2. Jasper Nalbach.
    Embedding the virtual substitution in the MCSAT framework
    Bachelor's Thesis. 2017.
    https://ths.rwth-aachen.de/wp-content/uploads/sites/4/teaching/theses/nalbach_bachelor.pdf

Talks

2025

  1. A Variant of Non-uniform Cylindrical Algebraic Decomposition for Real Quantifier Elimination
    10th International Workshop on Satisfiability Checking and Symbolic Computation, Stuttgart, Germany. August 2025.
    Slides
  2. Projective Delineability for Single Cell Construction
    10th International Workshop on Satisfiability Checking and Symbolic Computation, Stuttgart, Germany. August 2025.
    Slides

2024

  1. Merging Adjacent Cells During Single Cell Construction
    26th International Workshop on Computer Algebra in Scientific Computing, Rennes, France. September 2024.
    Slides
  2. Solving Quantified Non-linear Real Arithmetic using Cylindrical Algebraic Coverings
    9th International Workshop on Satisfiability Checking and Symbolic Computation, Nancy, France. July 2024.
    Slides

2023

  1. A Compositional Proof System for Cylindrical Algebraic Decomposition
    Dagstuhl Seminar 23471 "The Next Generation of Deduction Systems: From Composition to Compositionality", Dagstuhl, Germany. November 2023.
    Slides
  2. A Short Introduction to the Cylindrical Algebraic Decomposition
    Department of Information and Computing Sciences, Utrecht University, Utrecht, the Netherlands. November 2023.
    Slides
  3. Constructing single cylindrical algebraic cells
    Department of Computer Science, University of Bath, Bath, United Kingdom. August 2023.
    Slides
  4. Subtropical Satisfiability for SMT Solving
    15th International Symposium on NASA Formal Methods, Austin, Texas, United States (Remote Participation). May 2023.
    Slides

2022

  1. Levelwise construction of a single cylindrical algebraic cell
    Dagstuhl Seminar 22072 "New Perspectives in Symbolic Computation and Satisfiability Checking", Dagstuhl, Germany. July 2022.
    Slides

2021

  1. Extending the Fundamental Theorem of Linear Programming for Strict Inequalities
    6th International Workshop on Satisfiability Checking and Symbolic Computation, College Station, United States (Virtual Event). August 2021.
  2. Extending the Fundamental Theorem of Linear Programming for Strict Inequalities
    46th International Symposium on Symbolic and Algebraic Computation, Saint Petersburg, Russia (Virtual Event). July 2021.
    Slides

2019

  1. On Variable Orderings in MCSAT for Non-linear Real Arithmetic
    4th International Workshop on Satisfiability Checking and Symbolic Computation, Bern, Switzerland. July 2019.
    Slides

2017

  1. Embedding the Virtual Substitution Method in the Model Constructing Satisfiability Calculus Framework
    2nd International Workshop on Satisfiability Checking and Symbolic Computation, Kaiserslautern, Germany. July 2017.

Teaching Assistance

  • Satisfiability Checking
    Lecture
    WS20/21, WS21/22, WS22/23, WS23/24, WS24/25, WS25/26
  • Modeling and Analysis of Hybrid Systems
    Lecture
    SS21
  • Algorithmen und Datenstrukturen
    Lecture
    SS20, SS22
  • Satisfiability Checking
    Seminar
    SS20, WS20/21, SS21, WS21/22, SS22, SS23, SS25
  • Formale Methoden
    Proseminar
    WS20/21, SS21, WS21/22
  • Neural network verification with Reluplex
    Practical lab
    WS20/21

Advised Theses

2025

  1. Jan Bienmüller.
    Abstraction techniques in exploration-guided algorithms for real algebra
    Bachelor's Thesis. 2025.
    https://ths.rwth-aachen.de/wp-content/uploads/sites/4/Thesis_Jan_Bienmueller.pdf
  2. Alexej Kolbin.
    Traversal heuristics for cylindrical algebraic coverings
    Bachelor's Thesis. 2025.
    https://ths.rwth-aachen.de/wp-content/uploads/sites/4/thesis_Kolbin.pdf

2024

  1. Carsten Peter Perkampus.
    Speed up single cell construction via combinatorial optimization
    Bachelor's Thesis. 2024.
    https://ths.rwth-aachen.de/wp-content/uploads/sites/4/thesis_perkampus.pdf

2023

  1. Kristian Cović.
    Heuristical variable ordering in the cylindrical algebraic decomposition
    Bachelor's Thesis. 2023.
    https://ths.rwth-aachen.de/wp-content/uploads/sites/4/thesis_covic.pdf
  2. Philip Kroll.
    Implementation of cylindrical algebraic coverings for quantifier elimination
    Master's Thesis. 2023.
    https://ths.rwth-aachen.de/wp-content/uploads/sites/4/MasterPhilipKroll.pdf
  3. Philippe Specht.
    Improving incremental linearization for satisfiability modulo non-linear real arithmetic checking
    Master's Thesis. 2023.
    https://ths.rwth-aachen.de/wp-content/uploads/sites/4/master_specht.pdf
  4. Paul Tristan Wagner.
    Piecewise linear under-approximation of cell boundaries in MCSAT
    Bachelor's Thesis. 2023.
    https://ths.rwth-aachen.de/wp-content/uploads/sites/4/bachelor_thesis_paul_wagner.pdf

2022

  1. Philipp Bär.
    Exploiting strict constraints in the computations of cylindrical algebraic coverings
    Bachelor's Thesis. 2022.
    https://ths.rwth-aachen.de/wp-content/uploads/sites/4/bachelorarbeit-philipp-baer.pdf
  2. Max Harder.
    Generating coverings using virtual substitution for explanations in mcSAT
    Bachelor's Thesis. 2022.
    https://ths.rwth-aachen.de/wp-content/uploads/sites/4/Bachelorarbeit_MaxHarder.pdf
  3. Kai Hilgers.
    An FMplex-inspired simplex heuristics
    Bachelor's Thesis. 2022.
    https://ths.rwth-aachen.de/wp-content/uploads/sites/4/hilgers_bachelor.pdf
  4. Valentin Promies.
    Underapproximating cell bounds in MCSAT using low-degree polynomials
    Master's Thesis. 2022.
    https://ths.rwth-aachen.de/wp-content/uploads/sites/4/master_valentin_promies.pdf
  5. Svenja Stein.
    An incremental adaption of the FMPlex method for solving linear real algebraic formulas
    Bachelor's Thesis. 2022.
    https://ths.rwth-aachen.de/wp-content/uploads/sites/4/Bachelor_Stein_Svenja.pdf

2021

  1. Paul Kobialka.
    Connecting simplex and Fourier-Motzkin into a novel quantifier elimination method for linear real algebra
    Master's Thesis. 2021.
    https://ths.rwth-aachen.de/wp-content/uploads/sites/4/kobialka_master.pdf
  2. André Leon Poncelet.
    Conflict generalization for quadratic real-arithmetic constraints in SMT-RAT
    Bachelor's Thesis. 2021.
    https://ths.rwth-aachen.de/wp-content/uploads/sites/4/poncelet_bachelor.pdf

2020

  1. Fabian Alieff.
    Simplex heuristics in SMT solving
    Bachelor's Thesis. 2020.
    https://ths.rwth-aachen.de/wp-content/uploads/sites/4/alieff_bachelor.pdf
  2. Daniel Alexander Heinen.
    Purging spurious samples in the cylindrical algebraic decomposition
    Bachelor's Thesis. 2020.
    https://ths.rwth-aachen.de/wp-content/uploads/sites/4/heinen_bachelor.pdf
  3. Philip Kroll.
    Efficient data structures for cylindrical algebraic coverings
    Bachelor's Thesis. 2020.
    https://ths.rwth-aachen.de/wp-content/uploads/sites/4/kroll_bachelor.pdf
  4. Philippe Specht.
    A level-wise variant of single cell construction in cylindrical algebraic decomposition
    Bachelor's Thesis. 2020.
    https://ths.rwth-aachen.de/wp-content/uploads/sites/4/teaching/theses/specht_bachelor.pdf

All theses were supervised by Erika Ábrahám.

Other Activities

Conference Reviews

SC-square 2020, CAV 2021 (Artifact Evaluation Committee), FMCAD 2021, IJCAR 2022, ISSAC 2024, CAV 2024, FM 2024, CASC 2024, CAV 2025, SAT 2025, TACAS 2025, SMT 2025

Journal Reviews

MCS 2023 (SC-square)

PC member

SC-square 2025