Recent and upcoming events

• PC member of POPL 2025.
• Smoothness Analysis for Probabilistic Programs with Application to Optimised Variational Inference, ACM Symposium on Principles of Programming Languages (POPL 2023), 2023.
• On Correctness of Automatic Differentiation for Non-Differentiable Functions, NeurIPS 2020.
• Towards verified stochastic variational inference for probabilistic programs, ACM Symposium on Principles of Programming Languages (POPL 2020), 2020.
• POPL 2020, New Orleans, USA 2020 (Program Committee)
• Introduction to static analysis book published at MIT Press!
• Semantic-Directed Clumping of Disjunctive Abstract States, ACM Symposium on Principles of Programming Languages (POPL 2017), 2017 (VM).
• SAS 2016, Edinburgh, September 2016 (PC Chair)
• APLAS 2015, Pohang, South Korea, December 2015 (Program Committee)
• SAS 2014, Münich, Germany, September 2014 (Program Committee)
• VMCAI 2014, San Diego, USA, January 2014 (Program Committe Co-Chair)
• POPL 2014, San Diego, USA, January 2014 (Program Committee)

Research interests

I am working on static analysis for the verification of semantic properties of programs. My main focus is on abstract interpretation and more specifically on symbolic abstractions:

• Static Analysis by abstract interpretation, foundations and practical aspects of static analysis.
• Shape analysis
  
  • MemCAD ERC Project
  • the Xisa analyzer
• Static Analysis of embedded, safety critical software
  the Astrée project: static analysis, for proving the absence of runtime errors in safety critical embedded software.
  Commercial support by AbsInt (see here for more info).
• Static analysis of probabilistic programs.

In the past, I have also worked on the following topics. Although not currently working on these, I am still following new results in these areas.

• Certified compilation
  the Lcertify translation validator
• Slicing, dependence semantics
• Static analysis of Spreadsheet Applications
• Static analysis of JavaScript Software

Software

• MemCAD static analyzer, as part of the MemCAD ERC Project.
• Astrée static analyzer.
• LCertify translation validator library.

Projects

• VeriAMOS ANR Project.
• MemCAD ERC Project (ERC Starting Grant).
• MBAT.
• Astrée.
• AstréeA.
• ANR VerAsCo.
• ANR AnaStaSec.

Current PhD students

• Charles De Haro, PhD Student at ENS Paris
• Valentin Barbazo, PhD Student at ENS Paris
• Ignacio Tiraboschi, PhD Student at INRIA Paris, co-supervised with Tamara Rezk

Past PhD students

• Tie Cheng, PhD at ENS Paris, graduated in September 2015. Founder and CEO of MatrixLead.
• Antoine Toubhans
• Arlen Cox, PhD at University of Colorado at Boulder and ENS Paris, co-advised with Bor-Yuh Evan Chang, graduated in November 2014. Researcher in Formal Methods.
• Huisong Li, PhD at ENS Paris, graduated in March 2018. Developer at TrustInSoft.
• Jiangchao Liu, PhD at ENS Paris, graduated in February 2018. Assistant Professor at NUDT.
• Hugo Illous, PhD Student at CEA and ENS Paris, co-supervised with Matthieu Lemerre. Now engineer at Mathworks.
• Olivier Nicole, PhD Student at CEA and ENS Paris, co-supervised with Matthieu Lemerre. Now engineer at Tarides.
• Josselin giet, Now engineer at AbsInt Angewandte Informatik.

Teaching

• I teach a part of the Semantics and application to verification Course, in the first year of the Computer Science Curriculum at ENS of Paris.
• I teach a part of the Abstract Interpretation course, at the Master Parisien de Recherche en Informatique (MPRI) Master.

Address and contact information

DI - Ecole Normale Supérieure
45, rue d'Ulm
75230 Paris Cedex 05 - France

E-mail: rival A T di.ens.fr
Bureau: 2nd étage, "escalier de la direction", see the map
Phone: +33 1 44 32 21 50
Fax: +33 1 44 32 20 80

More information about me

• Photography