Jasper Nalbach

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

I am a doctoral student of the Theory of Hybrid Systems group and an associate member of the UnRAVeL training group since April 2020.

Research Interests

  • SMT solving
  • Nonlinear real arithmetic
  • Cylindrical Algebraic Decomposition
  • Linear arithmetic

Teaching Assistance

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

For supervised theses see here.


DOI arXiv:2212.09309 [bibtex]
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},
type = {Preprint},
year = {2023},
doi = {10.48550/arXiv.2212.09309},
url = { https://arxiv.org/abs/2212.09309},
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, 2023. https://arxiv.org/abs/2212.09309
DOI [bibtex]
title = {Automated Exercise Generation for Satisfiability Checking},
author = {Erika Ábrahám and Jasper 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},
Erika Ábrahám, Jasper Nalbach, Valentin Maxim Promies. Automated Exercise Generation for Satisfiability Checking, 5th International Workshop on Formal Methods Teaching (FMTea 2023), Volume 13962 of LNCS, 1-16, Springer, 2023.
title = {Cylindrical Algebraic Coverings for Quantifiers},
author = {Gereon Kremer and Jasper Kurt Ferdinand Nalbach},
type = {Conference Paper},
year = {2022},
url = { https://publications.rwth-aachen.de/record/956001},
Gereon Kremer, Jasper Kurt Ferdinand Nalbach. Cylindrical Algebraic Coverings for Quantifiers, Satisfiability Checking and Symbolic Computation (SC² 2022), 2022.
Show all