Solène MOREAU

I am a research engineer at Inria in the Toccata team, working on formal verification of properties of programs in the ProofInUse consortium under the supervision of Claude MARCHÉ.

More precisely, I am working on providing software verification tools based on the Why3 platform to industry users.

Before that, I was a PhD student under the supervision of Stéphanie DELAUNE and David BAELDE in the SPICY team (formerly EMSEC team) at IRISA in Rennes, working on formal methods for the verification of security and privacy in communication protocols.

I defended my PhD on November 18, 2021 (manuscript and defense slides).

Publications

• A method for proving unlinkability of stateful protocols - [HAL report]
  David BAELDE, Stéphanie DELAUNE, Solène MOREAU
  Accepted at CSF 2020 with award for "distinguished paper"


• An interactive prover for protocol verification in the computational model - [HAL report]
  David BAELDE, Stéphanie DELAUNE, Charlie JACOMME, Adrien KOUTSOS, Solène MOREAU
  Accepted at SP 2021


• Cracking the Stateful Nut -- Computational Proofs of Stateful Security Protocols using the Squirrel Proof Assistant - [HAL report]
  David BAELDE, Stéphanie DELAUNE, Adrien KOUTSOS, Solène MOREAU
  Accepted at CSF 2022

Tools

• During my PhD, I was involved in the development of the Squirrel Prover.
  


• As part of the ProofInUse consortium, I am contributing to the Why3 platform and to the proof tool of the SPARK 2014 environment developped by AdaCore.

Talks

• Verifying unlinkability, the case of stateful protocols
  David BAELDE, Stéphanie DELAUNE, Solène MOREAU
  
  • ANR TECAP meeting - July 08, 2019 - [slides]
  • EMSEC's team seminar - September 19, 2019
  • CSF 2020 - June 23, 2020 - [slides]


• An interactive prover for protocol verification in the computational model
  David BAELDE, Stéphanie DELAUNE, Charlie JACOMME, Adrien KOUTSOS, Solène MOREAU
  
  • EMSEC's team seminar - September 21, 2020
  • ANR TECAP meeting - October 15, 2020 - [slides]
  • BINSEC webinar - January 12, 2021

Teaching

2018-2019

• Introduction to imperative programming based on the Java language
  Université Rennes 1 - L1 Informatique
  Exercise courses (TD) and practical exercises (TP)


• Functional and immutable programming
  Université Rennes 1 - L1 Informatique
  Practical exercises (TP)

2019-2020

• Functional programming
  INSA - Spécialité Informatique 3ème année
  Practical exercises (TP)


• Functional and immutable programming
  Université Rennes 1 - L1 Informatique
  Practical exercises (TP)


• Deductive verification
  Université Rennes 1 - L3 Informatique
  Practical exercises (TP)

2020-2021

• Functional programming
  INSA - Spécialité Informatique 3ème année
  Practical exercises (TP)