Jasper Nalbach

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

I am a doctoral student of the Theory of Hybrid Systems group 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)
  • 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.

Publications

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), 4th 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, 2nd International Workshop on Satisfiability Checking and Symbolic Computation (SC2), Volume 1974 of CEUR Workshop Proceedings, 12 Seiten, RWTH Aachen, 2017.