Contract type : Fixed-term contract
Level of qualifications required : Graduate degree or equivalent
Other valued qualifications : Engineer degree
Fonction : Temporary scientific engineer
Level of experience : Recently graduated
Main goal: significantly enhance the IMITATOR software input syntax.
IMITATOR (www.imitator.fr) is a state-of-the-art software for formal verification of parametric timed models, with applications in the verification of real-time systems, as well as cybersecurity properties.
IMITATOR relies on the parametric timed automata formalism (an extension of finite-state automata), with some ad-hoc extensions such as shared rational variables. The goal is to significantly improve the set of types accepted by the tool, so as to allow a small programming language, including Booleans, integers, lists, arrays, user-defined functions, etc. A second direction will consist in allowing models parameterized by the number of components (e.g. a server with an arbitrary number of clients).
A more complete description of the subject is available at:
Under the supervision of Étienne André (full professor at LORIA) and in collaboration with the SED (development and experimentation service) of LORIA and, from time to time, with Jaime Arias (engineer with LIPN, Université Sorbonne Paris Nord), the hired person's main task will be to improve the IMITATOR input syntax. This consists in developing new types, and update consequently the core verification engine of IMITATOR.
For more information on the research topic:
IMITATOR is a parametric timed model checker. It takes as input models expressed using parametric timed automata, a formalism extending finite-state automata. The hired person will not need deep knowledge in this domain. Nevertheless, for information, links to the research domain are given below:
- model checking: en.wikipedia.org/wiki/Model_checking
- timed automata: en.wikipedia.org/wiki/Timed_automaton
- publications by Étienne André: www.loria.science/andre/
- VeriDis team research activities: team.inria.fr/veridis/
The hired person may developed an expertise in formal verification, a state-of-the-art domain with exciting perspectives in both the academic and industrial domains.
The hired person will be in charge of developing the IMITATOR syntax.
The hired person may have the responsibility to interact with IMITATOR users, including from the industry.
- software engineering
- OCaml development
- writing reports
- using and comparing other model checking software
Examples of activities:
- Analyze the designers and users' needs
- Interactions with the industrial and academic users of IMITATOR
- Prioritize and sort requests
- Propose an incremental development for the syntactic improvement
- Write documentation
- Test, modify, and validate
- Write reports
- Make presentations to the VeriDis team and other colleagues
- an engineer degree in computer science
- appreciated programming languages: OCaml, Python
- Linux OS environment
- English: be able to read and write documentation
Appreciated additional skills
- formal methods
- model checking
- Subsidized meals
- Partial reimbursement of public transport costs
- Leave: 7 weeks of annual leave + 10 extra days off due to RTT (statutory reduction in working hours) + possibility of exceptional leave (sick children, moving home, etc.)
- Possibility of teleworking (after 6 months of employment) and flexible organization of working hours
- Professional equipment available (videoconferencing, loan of computer equipment, etc.)
- Social, cultural and sports events and activities
- Access to vocational training
- Social security coverage
Rémunération : à partir de 2562 € brut mensuel selon diplôme et expérience.
- Theme/Domain :
Proofs and Verification
Software engineering (BAP E)
- Town/city : Villers lès Nancy
- Inria Center : CRI Nancy - Grand Est
- Starting date : 2021-01-01
- Duration of contract : 2 years
- Deadline to apply : 2020-10-31
The keys to success
The following skills are not compulsory, but mastering at least one of them will be a significant advantage for the application:
- mastering OCaml language
- formal methods
- model checking
- software engineering
- development in Python
Knowing French is not requested. English is of course compulsory.
Other appreciated skills:
- Enjoy working in a dynamic scientific environment
- Enjoy listening and talking
- A taste for software engineering
- Autonomy and ability to make technical suggestions
Inria is the French national research institute dedicated to digital science and technology. It employs 2,600 people. Its 200 agile project teams, generally run jointly with academic partners, include more than 3,500 scientists and engineers working to meet the challenges of digital technology, often at the interface with other disciplines. The Institute also employs numerous talents in over forty different professions. 900 research support staff contribute to the preparation and development of scientific and entrepreneurial projects that have a worldwide impact.
Instruction to apply
Defence Security :
This position is likely to be situated in a restricted area (ZRR), as defined in Decree No. 2011-1425 relating to the protection of national scientific and technical potential (PPST).Authorisation to enter an area is granted by the director of the unit, following a favourable Ministerial decision, as defined in the decree of 3 July 2012 relating to the PPST. An unfavourable Ministerial decision in respect of a position situated in a ZRR would result in the cancellation of the appointment.
Recruitment Policy :
As part of its diversity policy, all Inria positions are accessible to people with disabilities.
Warning : you must enter your e-mail address in order to save your application to Inria. Applications must be submitted online on the Inria website. Processing of applications sent from other channels is not guaranteed.