Jasper Nalbach

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

I am a PhD 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.

My research is on real algebra methods in SMT solving, with a strong focus on the cylindrical algebraic decomposition. I am developer of the SMT solver SMT-RAT.

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

2024

  1. 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 with Appendix)
    doi:10.5281/zenodo.5764569 (Artifact)
  2. 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
  3. 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 International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2023). 2023.
    doi:10.4204/EPTCS.390.2 (Open Access)
    doi:10.48550/arXiv.2309.03138 (Preprint with 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 with Appendix)
    doi:10.5281/zenodo.7900518 (Artifact)
  4. Gereon Kremer and Jasper Nalbach.
    Cylindrical Algebraic Coverings for Quantifiers
    In Satisfiability Checking and Symbolic Computation 2022 (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 International Symposium on Symbolic and Algebraic Computation (ISSAC ’21). 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 2019 (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

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
  • 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
  • Formale Methoden
    Proseminar
    WS20/21, SS21, WS21/22
  • Neural network verification with Reluplex
    Practical lab
    WS20/21

Supervised Theses

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 with 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

Journal Reviews

MCS 2023 (SC-square)