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 of embedded, safety critical softwares ( the Astree project )
• Shape analysis ( the Xisa analyzer )
• Abstract Interpretation
• Certified Compilation
• Slicing, dependence semantics

News

• 11th Conference on Verificaiton, Model Checking and Abstract Interpretation (VMCAI 2010). Submission deadline: August 21, 2009 (Abstracts due August 14, 2009).

• CV
• My thesis

Publications:

• Bor-Yuh Evan Chang and Xavier Rival. Relational Inductive Shape Analysis. In Principles Of Programming Languages 2008 (POPL'08).
• Xavier Rival and Laurent Mauborgne. Trace Partitioning in Abstract Interpretation Based Static Analyzers. In ACM Transactions On Programming Languages And Software (TOPLAS). July 2007.
• Bor-Yuh Evan Chang, Xavier Rival and George Necula. Shape Analysis with Structural Invariant Checkers. In Static Analysis Symposium 2007 (SAS'07).
• Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. Varieties of Static Analyzers: A Comparison with Astrée. In IFIP International Symposium on Theoretical Aspects of Software Engineering 2007 (TASE'07).
• Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. Combination of Abstractions in the Astrée static analyzer. In the 11th Annual Asian Comuting Science Conference (ASIAN 2006).
• 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]