Xavier Rival

Research Director at INRIA Paris (Directeur de Recherche, DR 1)

Head of the ANTIQUE (ANalyste staTIQUE) Project-Team

(formerly Abstraction Project-Team)

Recent and upcoming events

• 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 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).
• Shape analysis
  
  • MemCAD ERC Project
  • the Xisa analyzer
• Certified Compilation
  the Lcertify translation validator
• Abstract Interpretation
• Slicing, dependence semantics
• Verification 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

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.

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.
• I teach a part of the Protocol Safety and Verification, at the Advanced Computer Network Master
• I teach a part of the Program Verification, Experimental Course in the third year of the École Polytechnique
• I teach the lecture on "Programmation Avancée" (Advanced Programming) in the second year of the École Polytechnique

Address and contact information

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