Contract type : Public service fixed-term contract
Level of qualifications required : PhD or equivalent
Fonction : Post-Doctoral Research Visit
The ANR VeriAMOS project will attack the problem of verifying a class of Operating Systems services thanks to both Domain Specific Languages (DSL) and static analyzers. We will investigate whether the restricted expressiveness and the higher level of abstraction provided by the use of a DSL will make it possible to design static analyzers that can statically and fully automatically verify important classes of semantic properties on OS code, while retaining adequate performance of the OS service.
The VeriAMOS project is involving researchers from INRIA - Antique team, Whisper team, and UGA-LIG - Erods team.
The goal of the project to design a high-level, expressive DSL targeting the needs of I/O scheduling policies and it's implementation on top of a verified abstract machine. The approach will be first applied to the scheduling of I/Os for Solid-State Drives. The DSL compiler will generate C programs that use the primitives of the abstract machine. C generated code from the DSL and the abstract machine code will have to be verifiable by a static analyzer designed by the Antique team.
The postdoc fellow will be in charge of the design of the abstract machine, and it's implementation within the Linux kernel. This work will be carry on in coordination with the others project partners to support the execution of the C-code generated from the DSL programs and the verification of the C implementation.
*Required expertise and interests*
An experience in programming at the Linux kernel level is required. Interest or experience in program verification or static analysis is welcome.
- 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
- Gross Salary per month: 2 653€ brut/mensuel
- Theme/Domain :
Distributed Systems and middleware
System & Networks (BAP E)
- Town/city : Rennes
- Inria Center : CRI de Paris
- Starting date : 2019-11-01
- Duration of contract : 1 year, 4 months
- Deadline to apply : 2019-07-31
The keys to success
Linux kernel, C, Scheduling
Inria, the French national research institute for the digital sciences, promotes scientific excellence and technology transfer to maximise its impact. It employs 2,400 people. Its 200 agile project teams, generally with academic partners, involve more than 3,000 scientists in meeting the challenges of computer science and mathematics, often at the interface of other disciplines. Inria works with many companies and has assisted in the creation of over 160 startups. It strives to meet the challenges of the digital transformation of science, society and the economy.
Instruction to apply
- Letter of motivation highlighting the adequacy of the candidate's training with the proposed subject.
- List of publications.
- Thesis reports if the thesis has already been defended.
- For candidates who have not yet defended, an attestation from the thesis director with a progress report on the thesis / composition of the jury and the probable date of defense.
- Letters of recommendation
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.