Intern position in mechanized analysis of specifications

Intern position in mechanized analysis of specifications

The IMDEA Software Institute invites applications for intern positions

on the mechanized formal analysis of rich specification for highly

critical software.

Industrial requirements for critical systems are often modeled in

temporal specification languages with clean semantics. The main goal

of the internship is 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.

A second goal is to use the implementation of the operational

semantics to create tools that perform important tasks like

interpreters of the semantics, 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 a intern position at the IMDEA

Software Institute, Madrid, Spain.

Selected candidates will work with Pierre Ganty and Cesar Sanchez and

an international team of graduate students and researchers.

Who should apply?

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.

Working at IMDEA Software 

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.

Dates

The duration of the position will be at least 9 months.

How to apply?

Applicants interested in the position should submit their application

at https://careers.software.imdea.org/ using reference code

202301-mechspecs. Review of applications will begin immediately and

close when positions are filled or on February 15, 2023.

For enquiries about the position, please contact: pierre.ganty (at)

imdea.org or cesar.sanchez (at) imdea.org