Beware! This job offer is no longer valid, the position has been fulfilled.
The CONVECS team of Inria and LIG
is recruiting a PhD student
Start date: October 2015
Type of contract: Fixed term contract (CDD) for 3 years.
Salary: About 1600 EUR net per month (1950 EUR gross), health insurance included (French Social Security system).
Location: This thesis project will be carried out at the Inria Montbonnot site, about 10 kilometres from Grenoble.
Subject: « Debugging Concurrent Programs using Model Checking and Mining Techniques »
Recent computing trends promote the development of hardware and software applications that are intrinsically parallel, distributed, and concurrent. Designing and developing such systems has always been a tedious and error-prone task, and the ever increasing system complexity is making matters even worse. Although we are still far from proposing techniques and tools avoiding the existence of bugs in a system under development, we know how to automatically chase and find bugs that would be very difficult, if not impossible, to detect manually.
Model checking is an established technique for automatically verifying that a model, e.g., a Labelled Transition System (LTS), obtained from higher-level specification languages (such as process algebras) satisfies a given temporal property, e.g., the absence of deadlocks. When the model violates the property, the model checker returns a counterexample, which is a sequence of actions leading to a state where the property is not satisfied. Understanding this counterexample for debugging the specification is a complicated task for several reasons: (i) the counterexample can contain hundreds (even thousands) of actions, (ii) the debugging task is mostly achieved manually, and (iii) the counterexample does not give any clue on the state of the system (e.g., parallelism or data expressions) when the error occurs.
The objective of this project is to propose and develop new solutions for simplifying the comprehension of counterexamples and thus favouring usability of model checking techniques. To do so, we would like to apply pattern mining techniques to a set of correct traces (extracted from the LTS) and incorrect traces (corresponding to counterexamples), to identify specific patterns indicating more precisely the source of the problem.
CONVECS is a research team of Inria and the LIG laboratory. Its areas of expertise lie on formal verification techniques and tools for asynchronous concurrent systems. CONVECS is involved in several research directions: providing formal specification languages for describing concurrent systems; enhancing temporal logics and verification tools; fighting state explosion; designing generic components for verification, test, and performance evaluation; and demonstrating the applicability of its methods and tools on real-life applications with academic and industrial partnership. In particular, the members of CONVECS have been developing the CADP verification toolbox for about 25 years. CADP is dedicated to the design, analysis, and verification of asynchronous systems consisting of concurrent processes interacting via message passing.
This PhD thesis will be achieved in collaboration with the SLIDE research team of the LIG laboratory. SLIDE aims at combining efficient large-scale data processing with pattern mining algorithms to extract value from data. SLIDE's research is data-driven and the team develops algorithms and infrastructures for large-scale analytics, data linkage and ontology-based data access, crowd data sourcing and crowdsourced application evaluation. Working at the intersection of knowledge representation and reasoning, data mining, and data management, SLIDE operates on a variety of application domains such as the semantic and social Web, Health and well-being, Data center monitoring, and embedded systems.
Work proposed and expected results:
The candidate will complete the following tasks, among others:
Required skills and profile:
All questions concerning this thesis project should be addressed to:
Mr. Gwen Salaün
Inria Grenoble - Rhône-Alpes / CONVECS
655, avenue de l'Europe
38330 Montbonnot Saint-Martin
Tel : +33 (0)4 76 61 54 28
E-mail : Gwen.Salaun@inria.fr
Applications should be addressed directly to Gwen Salaün, preferably by e-mail, mentioning the position number #2015A. Applications received after July 8, 2015 might not be considered if a candidate has been selected already.