Jasper Nalbach

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 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, WS23/24)
  • Lecture: Modeling and Analysis of Hybrid Systems (SS21)
  • Lecture: Algorithmen und Datenstrukturen (SS20, SS22)
  • Seminar: Satisfiability Checking (SS20, WS20/21, SS21, WS21/22, SS22, SS24)
  • Proseminar: Formale Methoden (WS20/21, SS21, WS21/22)
  • Practical lab: Neural network verification with Reluplex (WS20/21)

For supervised theses see here.

Publications

ORCID

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.
2023
DOI arXiv:2212.09309 [bibtex]
@unpublished{L2023,
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},
}×
[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, 2023. https://arxiv.org/abs/2212.09309
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 [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},
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, 2023. https://arxiv.org/abs/2306.16757
DOI arXiv:2309.03138 [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},
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, 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.
2021
DOI [bibtex]
@conference{EFTLPSI2021,
title = {Extending the Fundamental Theorem of Linear Programming for Strict Inequalities},
author = {Jasper Kurt Ferdinand Nalbach and Erika Ábrahám and Gereon Kremer},
publisher = {Association for Computing Machinery},
booktitle = {ACM Conferences},
pages = {313-320},
type = {Conference Paper},
year = {2021},
doi = {10.1145/3452143.3465538},
url = { https://publications.rwth-aachen.de/record/823081},
}×
[issue] 		Jasper Kurt Ferdinand Nalbach, Erika Ábrahám, Gereon Kremer. Extending the Fundamental Theorem of Linear Programming for Strict Inequalities, International Symposium on Symbolic and Algebraic Computation (ISSAC '21), ACM Conferences, 313-320, Association for Computing Machinery, 2021.
2020
DOI fulltext PDF [bibtex]
@masterthesis{AS2020,
title = {A novel adaption of the Simplex algorithm for linear real arithmetic},
author = {Jasper Kurt Ferdinand Nalbach},
institution = {RWTH Aachen University},
pages = {79 Seiten},
type = {Master Thesis},
year = {2020},
doi = {10.18154/RWTH-2021-04303},
url = { https://publications.rwth-aachen.de/record/818122},
}×
[issue] 		Jasper Kurt Ferdinand Nalbach. A novel adaption of the Simplex algorithm for linear real arithmetic, Master Thesis, RWTH Aachen University, 79 Seiten, 2020.
2019
DOI fulltext PDF [bibtex]
@conference{OVOMNRA2019,
title = {On Variable Orderings in MCSAT for Non-linear Real Arithmetic: (extended abstract)},
author = {Jasper Kurt Ferdinand Nalbach and Gereon Kremer and Erika Ábrahám},
publisher = {RWTH Aachen},
booktitle = {CEUR Workshop Proceedings},
volume = {2460},
pages = {7 Seiten},
type = {Conference Paper},
year = {2019},
doi = {10.18154/RWTH-CONV-240068},
url = { https://publications.rwth-aachen.de/record/771622},
}×
[issue] 		Jasper Kurt Ferdinand Nalbach, Gereon Kremer, Erika Ábrahám. On Variable Orderings in MCSAT for Non-linear Real Arithmetic: (extended abstract), 4. Workshop on Satisfiability Checking and Symbolic Computation (SC-square), Volume 2460 of CEUR Workshop Proceedings, 7 Seiten, RWTH Aachen, 2019.
2017
[bibtex]
@conference{EVSMMCSCF2017,
title = {Embedding the Virtual Substitution Method in the Model Constructing Satisfiability Calculus Framework},
author = {Erika Ábrahám and Jasper Kurt Ferdinand Nalbach and Gereon Kremer},
publisher = {RWTH Aachen},
booktitle = {CEUR Workshop Proceedings},
volume = {1974},
pages = {12 Seiten},
type = {Conference Paper},
year = {2017},
url = { https://publications.rwth-aachen.de/record/713477},
}×
[issue] 		Erika Ábrahám, Jasper Kurt Ferdinand Nalbach, Gereon Kremer. Embedding the Virtual Substitution Method in the Model Constructing Satisfiability Calculus Framework, 2. International Workshop on Satisfiability Checking and Symbolic Computation (SC2), Volume 1974 of CEUR Workshop Proceedings, 12 Seiten, RWTH Aachen, 2017.