I'm interested in specification and verification of various non-functional properties for open embedded operating systems. More precisely, I'm working on the CAMILLE operating system (in collaboration with the RD2P team) and trying to perform some static analysis on the bytecode to ensure the validity of some properties, mostly related to security and optimization. See my thesis subject (in french) for more informations.
The complete thesis text is available here : public/hodique-phd.pdf
You may also want to have a look at a more complete bibliography
- “Approximations de stratégies de preuve en réécriture” (Master thesis, directed by Thomas Genet in the LANDE team) : conception of an algorithm permitting to build a sound strategy from a tree automaton that represents an over-estimation of the set of reachable terms.
- “Déploiement d'applications java”. Conception of a shell script able to mody the sources of a local program to make it a distributed application by injecting RMI code. Directed by David Simplot and Isabelle Ryl