Nicolas Palix

The ERODS research group is looking for a 18 month post-doctoral fellow. The work will take place in the LIG laboratory as an employee of the University of Grenoble - Alpes.

The gross salary will be of 2379 euros per month.

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 Paris - Antique team,
Sorbonne University - Whisper team, and UGA-LIG - Erods team.

The goal is to design a high-level, expressive DSL targeting the needs of I/O scheduling policies and to build a compiler that translates programs written in our DSL into C programs. The approach will be first applied to the scheduling of I/O for Solid-State Drives. The C-generated programs will use the primitives of the abstract machine defined by the Whisper team. The compiler must be designed to produce target code that is verifiable by automatic static analysis, using the VeriAMOS static analyzer provided by the Antique team.

The postdoc fellow will design the language together with some running examples. This work will be carry on in coordination with the others project partners to allow verification of the generated C code and the integration with the abstract machine. Finally, some performance evaluation and comparaison would be performed, leading to some optimisations.

Linux kernel, Domain-Specific Languages, OCaml, C, Scheduling

Nicolas Palix