Allan Blanchard

Person

Contact

Allan Blanchard
Inria Bat. A
40 avenue de Halley
F-59650 VILLENEUVE D'ASCQ

Join

About Me

I am currently a post-doc researcher at Inria Nord Europe for the EU H2020 VESSEDIA project. Previously, I was a teaching and research assistant (ATER) at the university institute of technology of Orléans, associated to the Laboratoire d'Informatique Fondamentale d'Orléans (LIFO). I prepared my PhD at the Software Reliability Laboratory of the CEA LIST.

Je suis actuellement post-doctorant à Inria Nord Europe pour le projet H2020 européen VESSEDIA. Précédemment, j'étais Attaché Temporaire d'Enseignement et de recherche (ATER) à l'IUT d'Orléans, rattaché au Laboratoire d'Informatique Fondamentale d'Orléans (LIFO). J'ai préparé ma thèse de doctorat au Laboratoire de Sûreté des Logiciels du CEA LIST.

Research/Recherche

I am interested in the analysis of concurrent code using formal methods and more precisely proof.

Currently, I am involved in the VESSEDIA project, that aims at making formal methods easier to apply in the context of the internet-of-things where many security risks are rising as IoT devices are more and more widespread. My current work is to apply formal verification to the Contiki microkernel (an lightweight OS for IoT) and its libraries, mostly to show the absence of runtime errors. I mostly use Frama-C with the EVA plugin and the WP plugin.

In the context of Contiki, concurrency is only simulated using a library called protothread which allows cooperative multi-tasking without the need of multiple stacks.

My PhD thesis work is about a (formally correct) code and specification transformation from concurrent to equivalent sequential code. It allows one to verify a concurrent code using tools dedicated to sequential code. Such a transformation is valid under the assumption that the verified program has a sequentially consistent behavior. Our processors implements memory models that do not guarantee it. A part of my work is to study these models, and to define ways to analyze programs taking them in account.

More details, publications ...


Je suis actuellement impliqué dans le projet VESSEDIA dont le but est de faciliter l'usage des méthodes formels pour le contexte de l'internet-of-things où les questions liées à la sécurité sont de plus en plus importantes à mesure que les systèmes IoT sont de plus en plus présents. Mes travaux actuels consistent à appliquer la vérification formelle au micronoyau Contiki (un OS léger pour l'IoT) et à ses bibliothèques, principalement pour montrer l'absence d'erreur à l'exécution. J'utilise principalement Frama-C avec les greffons EVA et WP.

Dans le contexte de Contiki, la concurrence est seulement simulée à l'aide d'une bibliothèque appelée protothread, qui permet de faire du multi-tâche collaboratif sans que cela ne nécessite plusieurs piles d'exécution.

Ma thèse porte sur une méthode d'aide à la vérification de programmes concurrents par transformation (formellement correcte) de code, et de spécification, vers du code séquentiel équivalent. On permet ainsi la validation de code concurrent avec des outils dédiés au séquentiel. Une telle méthode d'analyse n'est valide que dans le cas des programmes ayant un comportement séquentiellement consistant. Nos processeurs implémentent des modèles mémoires qui ne donnent pas une telle garantie. Une partie de mes travaux portent donc sur l'étude de ces modèles, et des moyens d'analyser les programmes en tenant compte de leurs spécificités.

Plus de détails, publications ...

Events/Événements

Upcoming/À venir:
  • 07/2018 - Program Committee : 4PAD 2018, Orléans, France []
  • 07/2018 - Tutorial : HPCS 2018, Orléans, France []
Past/Passés:
  • 06/2018 - Talk : TAP 2018, Toulouse, France [Slides]
  • 06/2018 - Talk : AFADL 2018, Grenoble, france [Slides]
  • 05/2018 - Tutorial : ZINC 2018, Novi Sad, Serbia [Slides]
  • 04/2018 - Talk : NFM 2018, Newport News, VA, USA [Slides]
  • 06/2017 - Talk : AFADL 2017, Montpellier, France [Slides]
  • 12/2016 : PhD Thesis Defence, Saclay, France [Slides]
  • 07/2016 - Talk : CSTVA 2016, Saarbrücken, Germany [Slides]
  • 06/2016 : Frama-C Day 2016, Paris, France [Poster]
  • 06/2015 - Talk : FMICS 2015, Oslo, Norway [Slides]
  • 06/2015 - Talk : AFADL 2015, Bordeaux, France [Slides]
  • 03/2015 : EJC IM 2015, Orléans, France [Slides]
  • 12/2014 : Forum STIC 2014, Saclay, France [Poster]
  • 06/2014 : EJCP 2014, Rennes, France

Teaching/Enseignement

I mainly teach code validation (using test and deductive proof), algorithms (basics, and then graphs and automaton), methods and languages for object-oriented design, and multi-core programmings (parallelism and concurrency).

More details.

La plupart de mes enseignements sont dans les thèmes de la validation de code (par test et par preuve déductive), l'algorithmique (bases puis graphes et automates), les méthodes et langages de conception orientée objet, ainsi que la programmation multi-coeur (parallélisme et concurrence).

Plus de détails.