Xavier Rival

Chargé de Recherche (Researcher) at INRIA

Contact:

E-mail: rival AT di.ens.fr
Bureau: S14
Phone: +33 1 44 32 21 50
Fax: +33 1 44 32 20 80

Research interests:

• Static Analysis ( the Astree project )
• Abstract Interpretation
• Certified Compilation
• Slicing, dependence semantics

CV

My thesis

Publications:

• Bor-Yuh Evan Chang and Xavier Rival. Relational Inductive Shape Analysis. In Principles Of Programming Languages 2008 (POPL'08). To appear.
• Xavier Rival. Abstract Dependences for Alarm Diagnosis In Asian Conference on Programming Languages And Software 2005 (APLAS'05) Lecture Notes in Computer Science. [.ps] [.pdf]

• Xavier Rival. Understanding the Origin of Alarms in Astrée In Static Analysis Symposium (SAS) 2005 Lecture Notes in Computer Science. [.ps] [.pdf]

• Laurent Mauborgne and Xavier Rival. Trace Partitioning in Abstract Interpretation Based Static Analyzers. In European Symposium On Programming (ESOP) 2005 Lecture Notes in Computer Science. [.ps] [.pdf]

• Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, Xavier Rival. The ASTRÉE Analyzer. In European Symposium On Programming (ESOP) 2005 Lecture Notes in Computer Science. [.ps] [.pdf]

• Xavier Rival. Invariant Translation-Based Certification of Assembly Code. In International Journal on Software and Tools for Technology Transfer Springer Verlag, 2004. [.ps] [.pdf]

• Xavier Rival. Symbolic Transfer Functions-based Approaches to Certified Compilation. In 31st Symposium on Principles of Programming Languages (POPL'2004), Venice, Jan. 2004 ACM. [.ps] [.pdf]

• Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux & Xavier Rival. A Static Analyzer for Large Safety-Critical Software . In ACM Programming Language Design and Implementation (PLDI 2003). [.ps] [.pdf]

• Xavier Rival Abstract Interpretation Based Certification of Assembly Code, In Proc. 4th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'2003), New York, Jan. 2003 Lecture Notes in Computer Science. [.ps] [.pdf]

• Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux & Xavier Rival. Design and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded Software, invited chapter. In The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones, T. Mogensen and D.A. Schmidt and I.H. Sudborough (Editors). Lecture Notes in Computer Science 2566, Springer. [.ps] [.pdf]

• Harry Mairson and Xavier Rival Proofnets and Context Semantics for the Additives In Proc. Computer Science Logic (CSL'02), Edinburgh, Scotland, Sep. 2002, Lecture Notes in Computer Science. Springer, 2002. [.ps]

• Xavier Rival and Jean Goubault-Larrecq. Experiments with finite tree automata in Coq. In Proc. 14th Int. Conf. Theorem Proving in Higher Order Logics (TPHOL'01), Edinburgh, Scotland, Sep. 2001, Lecture Notes in Computer Science. Springer, 2001. [.ps]