Research

I am a member of the TIMA laboratory, team VDS (since 2006). My main research interests are:

• Assertion-based verification of SystemC TLM models of Systems on Chip (ISIS tool), see here.
  [SIE12], [FM11], [MB11], [MEM10], [DAT10], [FDL09], [IDT08], [TC08]
  
  
• Application of formal methods (ACL2, PVS) to fault tolerance, FME3 project.
  [IT11], [DFT09], [ACL09], [SEL09]
  
  
• Formal verification of communications in Networks on Chips (NoC) with the ACL2 theorem prover (see here), and using Assertion-Based Verification.
  [NO12], [DDE10], [JES09], [SIC08], [NOC07]
  
  
• Test sequences generation to improve coverage in Assertion-Based Verification.
  [FDL11]
  
  

... and in the past:

• Combination of theorem proving/model checking methods for the formal verification of system-level designs.
  [AMAST04], [MEM03]
  
  
• Formal verification of circuits described in VHDL, a IEEE standard Hardware Description Language.
  Application of inductive theorem provers, in particular Nqthm (the Boyer-Moore Theorem Prover) and ACL2 (*).
  [D&T92], [SSM01], [NATO93], [BPS92], [CHA95], [EDAC94], [CHDL91]
  
  (*) See this announcement about the 2005 ACM Software System Award.
  
  
• Verification of high-level synthesis results: compositional formalization of Finite State Machines with Data Path (FSMD).
  [TVLSI00], [ICD98]
  
  
• Inductive proof of (the communication aspects of) distributed algorithms running on interconnection networks, Cayley graph-based representations, link with the MPI primitives.
  [PPL03], [FMPP02], [CHARME01], [LIM338]
  
  
• Inductive proof of replicated architectures: transformation of iterative VHDL descriptions into recursive functions, generalization of inductive theorems.
  [JCSC00], [FTP97], [FMPP97], [TPCD94], [CHDL93], [LIM290]
  
  
• Application of formal methods to the specification of communicating processes. In particular formal specification of the MPI (Message Passing Interface) standard using the Formal Description Technique LOTOS.
  [PDCS00], [Inv98], [EDTC96], [LIM337]
  
  
• Refinement-based design of iterative/recursive programs with the B Method (cooperation with Ludmila Klenova).
  [RCS02], [LIM368]
  
  

Interesting page on Formal Methods: Virtual Library: Formal Methods page

Tutorials and miscellaneous

Participation in FETCH'2013 (Ecole d'hiver Francophone sur les Technologies de Conception des Systèmes embarqués Hétérogènes), January 2013, presentation "Runtime verification of functional requirements for SoC models: integration of PSL in SystemC TLM", slides.

Participation in the Dagstuhl Seminar Verifying Reliability, August 2012, presentation "On the Use of Semi-Formal Methods for Reliability Analysis (at RT and TLM Abstraction Levels)". Dagstuhl report.

Participation in the panel "Low Power HW/SW Design: from Technology to Verification" of the MemoCODE'2010 conference, July 2010.

Invited talk on the formal verification of NoC infrastructures, at the Computer Laboratory of University of Cambridge (UK), in June 2008.

Invited talk (in French) on the integration of model-checking and theorem proving, at ENS Lyon, in March 2005.

Tutorial (in French) on ACL2, at Texas Instrument (Villeneuve-Loubet), in June 2003.

Tutorial on Nqthm and ACL2, at the Technical University of Darmstadt (Germany), in November 1999. Here are the slides.

Participation in the "Ecole des Jeunes Chercheurs en Programmation EJCP'99", Lille, March 1999.

Eric Gascard, Felix Nicoli and I took part in the "Inductive Theorem Proving Contest" organized in association with CADE-16 (Trento, Italy) in July 1999. See our results.