About me
I am a Phd working as an expert engineer at IRISA, in the Celtique team for the Serenitec project.
I am mainly interested in formal methods (static analysis, proof carrying code).
Contact
| Address | : IRISA, Projet Celtique, Campus de Beaulieu, 35042 Rennes Cedex France |
| : tiphaine[dot]turpin[at]irisa[dot]fr | |
| Phone | : +33 (0) 2 99 84 22 51 |
| Fax | : +33 (0) 2 99 84 71 71 |
Research
I have been working on three main topics: cryptographic protocol analysis, information flow analysis, and invariant pruning and reconstruction. My current activities consist in the design of a BDD-based solver for logic programs and its application to control flow analysis.Teaching
I have taught functional and imperative programming in L1-L2 (undergraduate curriculum) at University of Rennes 1, logics and computability in L3 at ENS Cachan, Ker Lann, lexical and syntactic analysis and advanced programming in the agrégation de mathématique at ENS Cachan.Software
- JavaLib : a library to access Java class files from Ocaml
- A prototype information flow analyser for Java bytecode
- Pruning algorithms for linear invariants generated by polyhedral analysis
- A Java bytecode verifier with pruning to take interfaces into account
- A BDD based solver for definite logic programs (work in progress)