The Max Planck Institute for Software Systems is looking for an enthusiastic and highly qualified
Doctoral Researcher (m/f/d)
to work in the intersection of formal methods, machine learning, and artificial intelligence. The open position is available in the Intelligent Formal Methods group under the supervision of Daniel Neider. It is part of the project Temporal Logic Sketching funded by the Deutsche Forschungsgemeinschaft (DFG). The position is to be filled on the next possible date.
Required Profile
- A candidate must have (or soon obtain) a Master's degree in Computer Science or a closely related area and have completed their studies with excellent grades.
- A strong background in formal methods, machine learning, or artificial intelligence is expected.
- A candidate should have had exposure to temporal logics such as Linear Temporal Logic (LTL), Signal Temporal Logic (STL), and Computational Tree Logic (CTL).
- Knowledge of automata learning, grammatical inference, and constraint solving (SAT and SMT) is preferred but not required.
Description of the Project and Position
The project Temporal Logic Sketching aims to fundamentally improve the way hardware and software engineers write formal specifications. It is predicated on the observation that virtually all of today's formal methods assume the (formal) specification used in the design or verification of a system to be available in a suitable format, to be functionally correct, and to express exactly the properties the developers had in mind—assumptions that are unrealistic in practice. In fact, formalizing system requirements is notoriously error-prone, and the training effort required to reach proficiency with formal specification languages can often be disproportionate to the expected benefits.
To mitigate this serious obstacle, the project Temporal Logic Sketching proposes a completely novel approach to writing formal specifications, which exploits that humans are usually very good at specifying high-level properties but often struggle with low-level details. The vision is that a future engineer may write a partial specification (a specification sketch) in which parts that are difficult to formalize can be omitted. Subsequently, an intelligent sketching tool would learn the missing parts of the specification by interacting with the developer (e.g., by querying the developer for examples of the system's desired behavior). In addition, the project will apply the developed techniques to interpretable machine learning and explainable artificial intelligence.
The doctoral researcher will be responsible for the development of such a sketching system, both in theory and as a proof-of-concept. The focus of the open position is on temporal specification languages, such as Linear Temporal Logic (LTL), Signal Temporal Logic (STL), and Computational Tree Logic (CTL), but may develop beyond that. The doctoral researcher will also have the opportunity to co-supervise an undergraduate student assistant, who will support the prototype implementation.
How to Apply
To apply, please submit a CV, a grade transcript, a research statement (or statement of purpose), and a list of references to
Please mention Temporal Logic Sketching in your application and send an email to Daniel Neider with your application ID. Review of applications will continue until the position is filled.
What we Offer
The Max Planck Institute for Software Systems (MPI-SWS) offers a vibrant international research environment with the possibility to participate in high-impact research. The institute is co-located in Kaiserslautern and Saarbrücken, Germany, and offers a multicultural and open working environment. The successful applicant will join the Intelligent Formal Methods group in Kaiserslautern. The working language at MPI-SWS is English. Proficiency in German is helpful but not required. You can find more information about MPI-SWS at https://www.mpi-sws.org.
The initial duration of the position is three years. The position is fully funded by the Deutsche Forschungsgemeinschaft (DFG) and pays according to the collective wage agreement of the German public service (TVöD).
Contact
Feel free to contact Daniel Neider for further information about the project and the position.