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.