Laurence PIERRE | TIMA - Université Grenoble Alpes

Full Professor (UGA)

Formal/semi-formal verification, Assertion-Based Verification for embedded systems, Runtime monitoring, SystemC models, Theorem proving

Education

PhD. in Applied Mathematics (Université Aix-Marseille)

Biography

I am a Full Professor of Computer Science with UFR IM2AG at Université Grenoble Alpes. Among my current and recent research activities:

Assertion-Based Verification of SystemC TLM models
Runtime monitoring of C programs (in the framework of the SPICA project)
In cooperation with Schneider Electric, high-level modeling and testing methods for cyber-physical system design
Test sequences generation to improve coverage in Assertion-Based Verification

Research

I am a member of the TIMA laboratory (since 2006), previously in the AMfoRS group and now in the SLS group (from April 2018).
Among my current and recent activities (see the references in the "Publications" tab):

Assertion-based verification of SystemC TLM models of Systems on Chip (ISIS tool), see here.
[INT21], [DSD17], [TOD16], [VL14], [IC14], [CO13], [SIE12], [FM11], [MB11], [MEM10], [DAT10], [FDL09], [IDT08], [TC08]
Runtime verification of C programs, in the framework of the SPICA project (OSIRIS tool), see here.
[MEM15], [DAT19]
In cooperation with Schneider Electric, high-level modeling and testing methods for cyber-physical system design.
[MO16], [FDL18]
Test sequences generation to improve coverage in Assertion-Based Verification.
[FDL15], [FDL11]

Previous activities:

Formal verification of communications in Networks on Chips (NoC) with the ACL2 theorem prover and using Assertion-Based Verification (see here).
[NO12], [DDE10], [JES09], [SIC08], [NOC07]
Application of formal methods (ACL2, PVS) to fault tolerance, FME3 project.
[IT11], [DFT09], [ACL09], [SEL09]
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]
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]

Interesting page on Formal Methods: Formal Methods Wiki

Main tutorials and invited talks

Participation in FETCH'2019 (Ecole d'hiver Francophone sur les Technologies de Conception des Systèmes embarqués Hétérogènes), January 2019, presentation "Runtime Assertion-Based Verification for Correctness and Reliability Analysis".

Participation in 2nd ARVI COST School on Runtime Verification, March 2018, presentation "Runtime Assertion-Based Verification for Hardware and Embedded Systems".

Participation in FETCH'2018 (Ecole d'hiver Francophone sur les Technologies de Conception des Systèmes embarqués Hétérogènes), January 2018, presentation "Verification of Cyber-physical Systems: from Requirements to Automated Tests".

Participation in Journée Vérification en ligne du matériel au logiciel of GDR SOC2, December 2017.

Participation in FETCH'2015 (Ecole d'hiver Francophone sur les Technologies de Conception des Systèmes embarqués Hétérogènes), January 2015, presentation "Runtime verification of embedded systems requirements throughout the design flow".

Participation in Forum Méthodes Formelles, "Preuve de modèle, preuve de programme" (Aerospace Valley - Minalogic), February 2014, tutorial "Outils de démonstration automatique et preuve de circuits électroniques".

Presentation at the TORRENTS working day (Time ORiented Reliable Embedded NeTworked Systems), December 2013, "Assertion-Based Verification for the validation and safety analysis of hardware/software systems on chip", slides.

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.

Projects - Conferences

Current and recent projects

FUI (Minalogic/SCS) Project SPICA (FUI17), 2014-2018
ANR Project SFINCS (coordinator)
ANR Project FME3 (coordinator)
FUI (Minalogic/Aerospace Valley) Project SoCKET
FUI (Minalogic) Project SHIVA

Involvement in Program Committees of recent or upcoming Conferences

"Design, Automation and Test in Europe" (DATE), Track D1 "System Specifications, Models, and Methodologies", from 2014 to 2018
"IEEE International Symposium on Design and Diagnostics of Electronic Circuits and Systems" since 2016, DDECS'2021 (April 2021)
"Forum on Specification and Design Languages" from 2010 to 2019
"IFIP/IEEE International Conference on Very Large Scale Integration" from 2011 to 2017, VLSI-SoC'2017 (October 2017)
Président du comité de programme du Track Architecture de la conférence Compas'2017 (Sophia-Antipolis, Juin 2017), participation au comité de programme du Track Architecture de Compas'2021
"Conference on Interactive Theorem Proving", ITP'2013 (Rennes, July 2013)
"IEEE International Design and Test Symposium", IDT'2012 and IDT'2013
"International Workshop on the ACL2 Theorem Prover and its Applications" 2007 (Austin, Nov. 2007), and 2011 (Austin, Nov. 2011, co-located with FMCAD'2011)
"IEEE International High Level Design Validation and Test Workshop", HLDVT'2010 (Anaheim Convention Center, co-located with DAC'2010, June 2010), HLDVT'2011 (Napa Valley, November 2011)

Mes enseignements à Grenoble (UJF, UGA)

Cours de Modélisation des systèmes numériques de IESE5 (Informatique et Electronique pour les Systèmes Embarqués, Polytech'Grenoble) et Master 2 EEATS MISTRE (Microélectronique, intégration des systèmes temps réel et embarqués), 2021-2022.
Course Embedded systems: from high-confidence design to safe execution of Master 2 MOSIG, 2021-2022.
Course Object-oriented and software design of M1 Master of Science in Industrial and Applied Mathematics, 2021-2022.
Cours et TD du Module Architectures Logicielles et Matérielles de la L3 Informatique, 2021-2022.
Cours du Module Système de la L3 MIAGE, 2021-2022.
Cours/TP dans l'option Méthodes et outils pour la conception avancée de la L3 Informatique, 2020-2021.
Cours/TD/TP du Module Introduction à la modélisation et à la vérification des systèmes numériques (option) du Master 1 Informatique et Master 1 MOSIG (Introduction to modeling and verification of digital systems), 2019-2020.
Cours/TD du Module Systèmes embarqués communicants pour l'Internet des objets (option, avec B.Tourancheau) du Master 2 Génie Informatique, jusqu'en 2018-2019.
Cours/TP du Module C pour la programmation système de RICM 3 (Réseaux Informatiques et Communication Multimédia, Polytech'Grenoble), jusqu'en 2017-2018.
Course High-confidence design: Industrial needs and processes of Master 2 MOSIG, HECS (High-confidence Embedded and Cyberphysical Systems), 2016-2017.
Cours, TD, TP du Module INF111 (Méthodes informatiques et techniques de programmation) de la Licence Sciences et Technologies, jusqu'en 2015.
TP du Module Réseaux du Master 1 Informatique, 2008-2010.

Formerly co-supervisor of HECS (High-confidence Embedded and Cyberphysical Systems), a specialization of Master 2 MOSIG.
Now involved in the Theme Software and hardware components engineering ; quality engineering, models of computation of MOSIG.

Mes enseignements à Nice, jusqu'en 2007

Cours du Module Introduction à la programmation C de Licence 1 MASS, 2006-2007.
Cours du Module I3 (Introduction à Caml) du Master 1 Informatique, 2006-2007.
Module UE9 (Modélisation et validation des systèmes numériques) du Master 2 STIC spécialité "Systèmes embarqués", 2007-2008.
Option Electronique Digitale du Master 1 Informatique, 2005-2006.
Cours du Module Introduction à la programmation Java de Licence 3 MASS, 2005-2006.
TP du Module Programmation orientée objet de la Licence 3 d'Informatique, 2005-2006.
Cours du Module I3 (Introductions à C++ et Caml) du Master 1 Informatique, 2005-2006.
Cours du Module L2' (approfondissement de l'étude du langage C) de la Licence d'Informatique, 2003-2004.
TP du Module L3' (programmation système) de la Licence d'Informatique, 2003-2004.

Quelques uns de mes enseignements en deuxième et troisième cycle à Marseille (Université de Provence), jusqu'en 2002

Cours de système UNIX et langage C en Licence d'Informatique, de 1995 à 1998, transparents en PostScript.
Cours de programmation orientée objet, en Maîtrise d'Informatique de 1992 à 1996, en DESS "Instrumentation, Capteurs, et Communications Industrielles" de 1997 à 2000, et dans le DTUP "IST" (maintenant Licence Professionnelle NTI) de 1998 à 2002.
Cours d'architecture des ordinateurs en Licence d'Informatique.
Cours de parallélisme (option) en Maîtrise d'Informatique.
Cours de modélisation des systèmes numériques et langage VHDL (option) en Maîtrise d'Informatique de 1996 à 2000.
Travaux Dirigés et Travaux Pratiques de réseaux en Maîtrise d'Informatique (administration, programmation client/serveur TCP/IP en C et JAVA).
Travaux Pratiques de programmation fonctionnelle (Lisp, Caml) en Maîtrise d'Informatique, et de logique en Licence d'Informatique.
Cours de vérification formelle des systèmes informatiques en DEA d'Informatique (thème "Systèmes parallèles et communicants").