I am a member of the
laboratory, team VDS (since 2006).
My main research interests are:
- Assertion-based verification of SystemC TLM models of
Systems on Chip (ISIS tool),
[SIE12], [FM11], [MB11], [MEM10], [DAT10], [FDL09], [IDT08], [TC08]
- Application of formal methods (ACL2, PVS) to fault tolerance,
[IT11], [DFT09], [ACL09], [SEL09]
- Formal verification of communications in Networks on
Chips (NoC) with the ACL2 theorem prover
and using Assertion-Based Verification.
[NO12], [DDE10], [JES09], [SIC08], [NOC07]
- Test sequences generation to improve coverage in
... and in the past:
- Combination of theorem proving/model checking
methods for the formal verification of system-level designs.
- Formal verification of circuits described
a IEEE standard Hardware Description Language.
Application of inductive theorem provers, in particular
(the Boyer-Moore Theorem Prover) and
[D&T92], [SSM01], [NATO93], [BPS92], [CHA95],
(*) 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).
- 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
Passing Interface) standard using the Formal Description Technique
[PDCS00], [Inv98], [EDTC96], [LIM337]
- Refinement-based design of iterative/recursive programs with the B Method (cooperation with Ludmila Klenova).
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",
Participation in the Dagstuhl Seminar
Reliability, August 2012, presentation "On the Use of Semi-Formal Methods for Reliability Analysis (at
RT and TLM Abstraction Levels)".
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.
Last modification January 13, 2013