The overall goal of the project is the formal implementation of novel rich languages for the specification of highly critical software. Industrial requirements for critical systems are often modeled in an adaptation of temporal logic that is amenable for specification and has clean semantics. The main goal of this part will be to implement the formal operational semantics of one concrete industrial specification language in a formal tool like Maude, K or as a translation into formal modeling languages like Alloy.
The second goal will be to use the implementation of the semantics to implement tools that perform important tasks like interpreting the semantics against inputs to the system, answers reachability queries (for example to be used for automated test generation) or detects contradictions.
The ideal candidate should have a strong background in logic, automata formal languages, and formal methods in general. Experience with tools like Maude, K, TLA+ or Alloy is a plus.
Selected PhD candidates will work with Pierre Ganty and César Sánchez and an international team of graduate students and researchers.
Who should apply?Candidates should hold a PhD in computer science or being close to complete one, have an interest in the above area as well as a promising publication record, and a strong commitment to research. Proven top programming skills as well as ability to understand and develop algorithms are required. Good teamwork and communication skills, including excellent spoken and written English are also required.
Working at IMDEA SoftwareThe positions are based in Madrid, Spain where the IMDEA Software Institute is situated. Salaries are internationally competitive and include attractive conditions such as access to an excellent public healthcare system. The working language at the institute is English. Knowledge of Spanish is not required.
DatesThe duration of the position will be 6 months. The ideal starting period is June 2023.
How to apply?Applicants interested in the position should submit their application at https: // careers.software.imdea.org/ using reference code 2023-03-phd- visiting-mechspecs. Deadline for applications is March 12th, 2023. Review of applications will begin immediately.
For enquiries about the position, please contact: pierre.ganty (at) imdea.org or cesar.sanchez (at) imdea.org