My name is Olivier Ponsini, since 2006 (and until October 2008), I work as a postdoctoral fellow in the VASY team of the french research institute INRIA located in Grenoble (INRIA Rhône-Alpes). VASY is also member of the Laboratoire d'Informatique de Grenoble (LIG).
Formerly, I did a PhD in computer science in the Langages team of the research laboratory I3S.
My complete cv is available as a pdf file (in french).
|
INRIA Rhône-Alpes 655, avenue de l'Europe F-38330 Montbonnot Saint-Martin FRANCE |
|
My research interests are focused on formal methods for software and hardware verification. In order to widespread and ease the use of formal methods for program and system verification, I have worked on translators from standard high-level programming or description languages into formal models more suitable to automated verification.
Now, I am working on integrating formal methods in new design flows based on transaction level models (SystemC/TLM). My main research direction is to investigate a semantic definition of TLM in a process algebra (LOTOS) that allows to use model-checking and equivalence checking to verify properties of the models (with the CADP toolbox). This involves studying asynchronous distributed systems and associated verification techniques. You can find more on this in my publications.
During my PhD, I worked on a system which automatically expresses, from source code, the semantics of imperative programs by a set of conditional equations. These equations can then be used in proof systems. This research involved studying semantics of programming languages, automated deduction, theorem proving, rewriting, fundamentals of computing and logic. You can find more on this in my publications. The software can be downloaded.