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.
Applications are invited to apply for an intern position at the IMDEA Software Institute, Madrid, Spain.
Selected candidates will work with Pierre Ganty and César Sánchez and an international team of graduate students and researchers.
Candidates should have a MSc or BSc degree (or be close to complete one) in computer science, mathematics, or a related discipline, with an interest in the above area, 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.
The position is based in Madrid, Spain, where the IMDEA Software Institute is situated. The institute provides for travel expenses and an internationally competitive stipend. The working language at the IMDEA Software Institute is English.
The duration of the position will be 9 months.
Applicants interested in the position should submit their application at https://careers.software.imdea.org/ using reference code 2023-01-intern-mechspecs. Review of applications will begin immediately and close when positions are filled or on February 15th, 2023.
For enquiries about the position, please contact: or
