My name is Olivier Ponsini, I am a research assistant at I3S Laboratory, located in Sophia Antipolis, in the CeP team.
From October 2006 to October 2008, I worked at INRIA (a french research institute) as a research assistant in the VASY project-team located in Grenoble (INRIA Rhône-Alpes). I was also a member of the Laboratoire d'Informatique de Grenoble (LIG).
I hold a PhD in computer science from the University of Nice - Sophia Antipolis. I prepared my thesis in the Langages (now Airelles) team of the I3S research laboratory.
My complete cv is available as a pdf file (in french).
|
Laboratoire I3S 2000 route des Lucioles Les Algorithmes bât. Euclide B 06 903 Sophia Antipolis Cedex 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.
My recent work takes place in the VACSIM ANR project. I am working on bounded model checking based on constraint programming techniques. I investigate verification of floating-point computations, fault-localization and heuristics for model-checking.
My previous work took place in the TESTEC and CAVERN ANR projects. I was also involved in the mancoosi european project. I studied optimization of loop handling in a bounded approach to imperative program verification. The approach was based on constraint programming. I worked on integrating inductive loop invariants as new constraints in order to avoid loop unfoldings. I also started working on verification of floating-point computations and heuristics for bounded model checking.
As a postdoctoral fellow, I worked on integrating formal methods in new design flows based on transaction level models (SystemC/TLM). My main research direction was 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 involved 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.