Jasper Nalbach

Dr.

nalbach
Email
nalbach at cs.rwth-aachen.de
Phone
+49 241 80 21246
Address
Room 4228
Ahornstraße 55
D-52074 Aachen

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 Assistance

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

For supervised theses see here and my website.

Publications

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

The following list is currently incomplete.

2024
DOI fulltext PDF [bibtex]
@article{L2024,
title = {Levelwise construction of a single cylindrical algebraic cell},
author = {Jasper Kurt Ferdinand Nalbach and Erika Ábrahám and Philippe Specht and Christopher W. Brown and James H. Davenport and Matthew England},
publisher = {Elsevier},
journal = {Journal of symbolic computation},
volume = {123},
pages = {pages 102288},
type = {Journal Article},
year = {2024},
doi = {10.1016/j.jsc.2023.102288},
url = { https://publications.rwth-aachen.de/record/975125},
}×
[issue] 		Jasper Kurt Ferdinand Nalbach, Erika Ábrahám, Philippe Specht, Christopher W. Brown, James H. Davenport, Matthew England. Levelwise construction of a single cylindrical algebraic cell, Journal of symbolic computation 123, pages 102288, Elsevier, 2024.
DOI [bibtex]
@conference{MACDSCC2024,
title = {Merging Adjacent Cells During Single Cell Construction},
author = {Jasper Kurt Ferdinand Nalbach and Erika Ábrahám},
publisher = {Springer},
booktitle = {LNCS},
volume = {14938},
pages = {252-272},
type = {Conference Paper},
year = {2024},
doi = {10.1007/978-3-031-69070-9_15},
url = { https://publications.rwth-aachen.de/record/991681},
}×
[issue] 		Jasper Kurt Ferdinand Nalbach, Erika Ábrahám. Merging Adjacent Cells During Single Cell Construction, 25. International Workshop on Computer Algebra in Scientific Computing (CASC 2024), Volume 14938 of LNCS, 252-272, Springer, 2024.
fulltext PDF [bibtex]
@misc{UASACEA2024,
title = {Under-Approximation of a Single Algebraic Cell (Extended Abstract)},
author = {Valentin Maxim Promies and Jasper Kurt Ferdinand Nalbach and Erika Ábrahám},
publisher = {RWTH Aachen},
booktitle = {CEUR workshop proceedings},
volume = {3717},
pages = {132-136},
type = {Invited Abstract},
year = {2024},
url = { https://publications.rwth-aachen.de/record/994020},
}×
[issue] 		Valentin Maxim Promies, Jasper Kurt Ferdinand Nalbach, Erika Ábrahám. Under-Approximation of a Single Algebraic Cell (Extended Abstract), Volume 3717 of CEUR workshop proceedings, 132-136, RWTH Aachen, 2024.
DOI arXiv:2411.13300 [bibtex]
@unpublished{OPD2024,
title = {On Projective Delineability},
author = {Lucas Michel and Jasper Kurt Ferdinand Nalbach and Pierre Mathonet and Naïm Zénaïdi and Christopher W. Brown and Erika Ábrahám and James H. Davenport and Matthew England},
type = {Preprint},
year = {2024},
doi = {10.48550/ARXIV.2411.13300},
url = { https://arxiv.org/abs/2411.13300},
}×
[issue] 		Lucas Michel, Jasper Kurt Ferdinand Nalbach, Pierre Mathonet, Naïm Zénaïdi, Christopher W. Brown, Erika Ábrahám, James H. Davenport, Matthew England. On Projective Delineability, 2024. https://arxiv.org/abs/2411.13300
DOI arXiv:2411.03070 [bibtex]
@unpublished{ECACMQ2024,
title = {Extensions of the Cylindrical Algebraic Covering Method for Quantifier},
author = {Jasper Kurt Ferdinand Nalbach and Gereon Kremer},
type = {Preprint},
year = {2024},
doi = {10.48550/ARXIV.2411.03070},
url = { https://arxiv.org/abs/2411.03070},
}×
[issue] 		Jasper Kurt Ferdinand Nalbach, Gereon Kremer. Extensions of the Cylindrical Algebraic Covering Method for Quantifier, 2024. https://arxiv.org/abs/2411.03070
2023
fulltext PDF [bibtex]
@conference{CACQ2023,
title = {Cylindrical Algebraic Coverings for Quantifiers},
author = {Gereon Kremer and Jasper Kurt Ferdinand Nalbach},
booktitle = {CEUR Workshop Proceedings},
volume = {3458},
pages = {9 Seiten},
type = {Conference Paper},
year = {2023},
url = { https://publications.rwth-aachen.de/record/956001},
}×
[issue] 		Gereon Kremer, Jasper Kurt Ferdinand Nalbach. Cylindrical Algebraic Coverings for Quantifiers, 7. International Workshop on Satisfiability Checking and Symbolic Computation (SC² 2022), Volume 3458 of CEUR Workshop Proceedings, 9 Seiten, 2023.
DOI [bibtex]
@conference{AEGSC2023,
title = {Automated Exercise Generation for Satisfiability Checking},
author = {Erika Ábrahám and Jasper Kurt Ferdinand Nalbach and Valentin Maxim Promies},
publisher = {Springer},
booktitle = {LNCS},
volume = {13962},
pages = {1-16},
type = {Conference Paper},
year = {2023},
doi = {10.1007/978-3-031-27534-0_1},
url = { https://publications.rwth-aachen.de/record/957774},
}×
[issue] 		Erika Ábrahám, Jasper Kurt Ferdinand Nalbach, Valentin Maxim Promies. Automated Exercise Generation for Satisfiability Checking, 5. International Workshop on Formal Methods Teaching (FMTea 2023), Volume 13962 of LNCS, 1-16, Springer, 2023.
DOI [bibtex]
@inbook{SSSS2023,
title = {Subtropical Satisfiability for SMT Solving},
author = {Jasper Kurt Ferdinand Nalbach and Erika Ábrahám},
publisher = {Springer},
booktitle = {LNCS},
volume = {13903},
pages = {430-446},
type = {Book Chapter},
year = {2023},
doi = {10.1007/978-3-031-33170-1_26},
url = { https://publications.rwth-aachen.de/record/960581},
}×
[issue] 		Jasper Kurt Ferdinand Nalbach, Erika Ábrahám. Subtropical Satisfiability for SMT Solving, Volume 13903 of LNCS, 430-446, Springer, 2023.
fulltext PDF [bibtex]
@conference{ESCCAC2023,
title = {Exploiting Strict Constraints in the Cylindrical Algebraic Covering},
author = {Philipp Bär and Jasper Kurt Ferdinand Nalbach and Erika Ábrahám and Christopher Brown},
booktitle = {CEUR workshop proceedings},
volume = {3429},
pages = {13 Seiten},
type = {Conference Paper},
year = {2023},
url = { https://publications.rwth-aachen.de/record/961989},
}×
[issue] 		Philipp Bär, Jasper Kurt Ferdinand Nalbach, Erika Ábrahám, Christopher Brown. Exploiting Strict Constraints in the Cylindrical Algebraic Covering, 21. International Workshop on Satisfiability Modulo Theories (SMT 2023), Volume 3429 of CEUR workshop proceedings, 13 Seiten, 2023.
DOI arXiv:2306.16757 fulltext PDF [bibtex]
@unpublished{ESCCAC2023,
title = {Exploiting Strict Constraints in the Cylindrical Algebraic Covering},
author = {Philipp Bär and Jasper Kurt Ferdinand Nalbach and Erika Ábrahám and Christopher W. Brown},
pages = {17 Seiten},
type = {Preprint},
year = {2023},
doi = {10.48550/arXiv.2306.16757},
url = { https://arxiv.org/abs/2306.16757},
}×
[issue] 		Philipp Bär, Jasper Kurt Ferdinand Nalbach, Erika Ábrahám, Christopher W. Brown. Exploiting Strict Constraints in the Cylindrical Algebraic Covering, 17 Seiten, 2023. https://arxiv.org/abs/2306.16757
DOI arXiv:2309.03138 fulltext PDF [bibtex]
@unpublished{FANMSLRAP2023,
title = {FMplex: A Novel Method for Solving Linear Real Arithmetic Problems},
author = {Jasper Kurt Ferdinand Nalbach and Valentin Maxim Promies and Erika Ábrahám and Paul Kobialka},
pages = {18 Seiten},
type = {Preprint},
year = {2023},
doi = {10.48550/arXiv.2309.03138},
url = { https://arxiv.org/abs/2309.03138},
}×
[issue] 		Jasper Kurt Ferdinand Nalbach, Valentin Maxim Promies, Erika Ábrahám, Paul Kobialka. FMplex: A Novel Method for Solving Linear Real Arithmetic Problems, 18 Seiten, 2023. https://arxiv.org/abs/2309.03138
DOI fulltext PDF [bibtex]
@conference{FANMSLRAP2023,
title = {FMplex: A Novel Method for Solving Linear Real Arithmetic Problems},
author = {Jasper Kurt Ferdinand Nalbach and Valentin Maxim Promies and Erika Ábrahám and Paul Kobialka},
publisher = {Open Publishing Association},
booktitle = {EPTCS},
volume = {390},
type = {Conference Paper},
year = {2023},
doi = {10.4204/EPTCS.390.2},
url = { https://publications.rwth-aachen.de/record/972368},
}×
[issue] 		Jasper Kurt Ferdinand Nalbach, Valentin Maxim Promies, Erika Ábrahám, Paul Kobialka. FMplex: A Novel Method for Solving Linear Real Arithmetic Problems, Fourteenth International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2023), Volume 390 of EPTCS, Open Publishing Association, 2023.
Show all