The young investigator group on Scalable Automated Reasoning at the Department of Informatics at the Karlsruhe Institute of Technology (KIT, in Germany) is looking for a research assistant (a.k.a. doctoral researcher, PhD student), beginning as soon as possible.

We intend the doctoral research to focus on one of the following subjects (to be determined together with the candidate):

• Increase the scalability of parallel and distributed SAT solving systems by fostering cooperation across solver threads and reducing the redundant work they perform.

• Investigate how to leverage the power of modern distributed SAT solving and task scheduling methods for Bounded Model Checking (BMC), a central verification technique.

• Transfer recent and ongoing advancements of distributed SAT solving to SMT (Satisfiability Modulo Theories), a powerful and highly popular extension of SAT to first-order logic.

A degree qualifying for doctoral studies in computer science (M.Sc. Computer Science or similar) with good grades is required. Prior specialization in formal methods, algorithms, and/or parallel and distributed computing is desirable. Good programming skills, in particular with C++, are highly recommended or should be acquired rapidly. The candidate will be supervised by Dr. Dominik Schreiber and co-supervised by Prof. Peter Sanders. The position is full-time, compensated according to TVÖD E13, and funded until (at least) 12/2027.

The full advertisement with further details can be found at: https://s.kit.edu/satres-phd Please direct your informal application / statement of interest together with any questions you may have to Dominik Schreiber dominik.schreiber@kit.edu. We are looking forward to hearing from you!