Coordinates

Sébastien Briais
PRISM-UVSQ
Bureau 414
45, avenue des États-Unis
F-78000 Versailles
France

01 39 25 44 26
Skype:

Research Engineer in the ARPA team.
Curriculum Vitae (fr|en)

Publications

Conferences:
- Mobile Objects "Must" Move Safely (pdf), S. Briais and U. Nestmann. In Proceedings of FMOODS 2002 (Twente, NL).
- Symbolic Bisimulations in the Spi Calculus (pdf), J. Borgström, S. Briais and U. Nestmann. In Proceedings of CONCUR 2004 (London, UK).
- A Formal Semantics for Protocol Narrations (pdf), S. Briais and U. Nestmann. In Proceedings of TGC'05 (Edinburgh, UK).
- Open Bisimulation, Revisited (pdf), S. Briais and U. Nestmann. In Proceedings of Express'05 (San Francisco, USA).
Journals:
- Open Bisimulation, Revisited , S. Briais and U. Nestmann. In Theoretical Computer Science, Volume 386, Issue 3 (November 2007).
- A Formal Semantics for Protocols Narrations , S. Briais and U. Nestmann. In Theoretical Computer Science, Volume 389, Issue 3 (December 2007).
Thesis:
- Theory and Tool Support for the Formal Verification of Cryptographic Protocols. PhD Thesis, École Polytechnique Fédérale de Lausanne, Switzerland, January 2008.
  The composition of the jury was the following:
  - Paolo Ienne, President
  - Dale Miller, External Rapporteur
  - Daniel Hirschkoff, External Rapporteur
  - Victor Kuncak, Internal Rapporteur
  - Martin Odersky, Thesis Director
  - Uwe Nestmann, Thesis Director
Technical reports:
- A Symbolic Characterisation of Open Bisimulation for the Spi Calculus (pdf), S. Briais (May 2007).
- Experimental Study of Register Saturation in Basic Blocks and Super-Blocks: Optimality and heuristics, S. Briais and S. Touati (November 2009).
- Schedule-Sensitive Register Pressure Reduction in Innermost Loops, Basic Blocks and Super-Blocks, S. Briais and S. Touati (November 2009).
- The Speedup Test, S. Touati and J. Worms and S. Briais (January 2010).
Talks:
- A Formal Semantics For Protocols Narrations (pdf), given at TGC05.
- Open Bisimulation, Revisited (pdf), given at Express'05.
- Open Bisimulation, Revisited (pdf), given as a Comète-Parsifal seminar at Lix.
- Une bisimulation ouverte pour le spi calcul (pdf), given as a Plume seminar at ENS Lyon.
- A Formalization of the Spi Calculus in Coq (pdf), given as a MSR-INRIA seminar at the MSR-INRIA joint centre.
- Theory and Tool Support for the Formal Verification of Cryptographic Protocols (pdf). Private/Public thesis defense.

Softwares

grappe (version 3.0)
ABC: Another Bisimulation Checker
spyer: a cryptographic protocol compiler
sbc: Symbolic Bisimulation Checker
A Formalisation of the Spi Calculus in Coq
Finite Automata Theory in Coq
The Fundamental Theorem of Arithmetic in Coq (old deprecated version)
SCEDA is a C library that provides efficient implementation of common data structures such as sets, maps, heaps, graphs as well as standard graph algorithms.

Teaching

Theoretical Computer Science 3 (Informatique Théorique 3), academic year 2004 (in french), given by U. Nestmann.
Course notes: U. Nestmann, S. Briais and D. Bünzli
Exercises and exam: S. Briais and D. Bünzli
Concurrency: Theory, Languages and Programming, academic year 2003, given by M. Odersky and U. Nestmann.
An exercise using the ABC
eins compiler (see Compiler Construction course 2004)
risc emulator
Cours de Projet - L3IF - ENS Lyon (2007)

validator.w3.org