Xavier Rival's publications
- Shape Analysis.
Bor-Yuh Evan Chang, Cezara Dragoi, Roman Manevich, Noam Rinetzky,
Xavier Rival.
In Foundations and Trends in Programming Languages
(FNT), 6(1-2): 1-158 (2020).
([.pdf])
- Towards verified stochastic
variational inference for probabilistic programs.
Wonyeol Lee, Hangyeol Yu, Xavier Rival, Hongseok Yang.
In Symposium on Principles of Programming Languages
(POPL 2020), New Orleans, USA and PACML, 16:1-16:33 (2020).
([.pdf])
- On Correctness of Automatic
Differentiation for Non-Differentiable Functions.
Wonyeol Lee, Hangyeol Yu, Xavier Rival, Hongseok Yang
In NeurIPS 2020.
([.pdf])
- Interprocedural Shape Analysis
Using Separation Logic-Based Transformer Summaries.
Hugo Illous, Matthieu Lemerre, Xavier Rival.
In Static Analysis Symposium (SAS 20), 248-273.
([.pdf])
- Weakly Sensitive Analysis for
Unbounded Iteration over JavaScript Objects.
Yoonseok Ko, Xavier Rival, Sukyoung Ryu.
In Asian Conference on Programming Languages And
Software (APLAS 15),
Kyoto (Japon), December 2017, Lecture Notes in
Computer Science 10695,
pages 148--168, Springer.
([.pdf])
- An array content static
analysis based on non-contiguous partitions.
Jiangchao Liu, Xavier Rival.
In Computer Languages, Systems and Structures (COMLAN)
47: 104-129 (2017).
([.pdf])
- A Relational Shape Abstract Domain.
Hugo Illous, Matthieu Lemerre and Xavier Rival.
In Nasa Formal Methods Symposium (NFM 17).
([.pdf])
- Semantic-Directed Clumping of
Disjunctive Abstract States, ACM Symposium on Principles
of Programming Languages (POPL 2017), 2017
Huisong Li, Francois Berenger, Bor-Yuh Evan Chang
and Xavier Rival.
In Principles Of Programming Languages 2017 (POPL 17),
Paris, Jan. 2017.
([.pdf],
VM).
- Static Analysis and Verification
of Aerospace Software by Abstract Interpretation.
Julien Bertrane, Patrick Cousot, Radhia Cousot,
Jéròme Feret, Laurent Mauborgne,
Antoine Miné, and Xavier Rival.
In Foundations and Trends in Programming Languages
(FNT).
([.pdf])
- Abstraction of Optional
Numerical Values.
Jiangchao Liu and Xavier Rival.
In Asian Conference on Programming Languages And
Software (APLAS 15),
Pohang (South Korea), December 2015, Lecture Notes in
Computer Science 9458,
pages 146--166, Springer.
[.pdf]
- Abstract Domains and Solvers for Sets
Reasoning.
Arlen Cox, Bor-Yuh Evan Chang, Huisong Li and Xavier Rival.
In Logic for Programming, Artificial Intelligence, and Reasoning
(LPAR 15), Suva (Fidji), December 2015,
Lecture Notes in Computer Science 9450, pages 356--371, Springer.
[.pdf]
- Shape Analysis for Unstructured Sharing.
Huisong Li, Xavier Rival, Bor-Yuh Evan Chang.
In Static Analysis Symposium (SAS 15), Saint-Malo (France), September 2015,
Lecture Notes in Computer Science 9291, pages 90--108, Springer.
[.pdf]
- Desynchronized Multi-State Abstractions for Open Programs
in Dynamic Languages.
Arlen Cox, Bor-Yuh Evan Chang and Xavier Rival.
In European Symposium On Programming (ESOP 15), London (UK), April 2015.
[.pdf] (to appear).
- Static Analysis of Spreadsheet Applications for
the Detection of Type Unsafe Operations.
Tie Cheng and Xavier Rival,
In European Symposium On Programming (ESOP 15), London (UK), April 2015.
[.pdf] (to appear).
- Abstraction of Arrays Based on Non-Contiguous Partitions.
Jiangchao Liu and Xavier Rival,
In Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 15),
Mumbai (India), January 2015, Lecture Notes in Computer Science 8931, pages 375--395, Springer.
[.pdf].
- Construction of Abstract Domains for Heterogeneous Properties.
Antoine Toubhans, Bor-Yuh Evan Chang and Xavier Rival,
In International Symposium On Leveraging Applications of Formal Methods, Verification and
Validation (ISOLA'14),
Corfu (Greece), October 2014, Lecture Notes in Computer Science 8803, pages 489--492, Springer.
[.pdf].
- Automatic Analysis of Open Objects in Dynamic Language
Programs.
Arlen Cox, Bor-Yuh Evan Chang and Xavier Rival,
In Static Analysis Symposium (SAS'14), Muenchen (Germany), September 2014,
Lecture Notes in Computer Science
8723, pages 285--301, Springer.
[.pdf].
- An Abstract Domain Combinator for Separately Conjoining Memory
Abstractions.
Antoine Toubhans, Bor-Yuh Evan Chang and Xavier Rival,
In Static Analysis Symposium (SAS'14), Muenchen (Germany), September 2014,
Lecture Notes in Computer Science 8723, pages 285--301, Springer.
[.pdf].
- Static Analysis by Abstract Interpretation of Embedded
Critical Software.
Julien Bertrane, Patrick Cousot, Radhia Cousot, Jéròme Feret,
Laurent Mauborgne, Antoine Miné, and Xavier Rival.
In Third IEEE International workshop UML and Formal Methods, 16 November 2010, Shanghai, China
[.pdf]
- Concrete Memory Models for Shape Analysis.
Pascal Sotin, Bertrand Jeannet, and Xavier Rival.
In The Second International Workshop on Numerical and Symbolic
Abstract Domains (NSAD 2010), ENTCS.
September 2010.
[.pdf]
- Astrée: Proving the Absence of Runtime Errors.
Daniel Kaestner, Stephan Wilhelm, Stefana Nenova, Patrick Cousot,
Radhia Cousot, Jérôme Feret, Laurent Mauborgne,
Antoine Miné and Xavier Rival.
In Embedded Real Time Software and Systems (ERTS 2010).
[.pdf]
- Static Analysis and Verification of Aerospace Software
by Abstract Interpretation.
Julien Bertrane, Patrick Cousot, Radhia Cousot, Jérôme Feret,
Laurent Mauborgne, Antoine Miné and Xavier Rival.
In American Institute of Aeronautics and Astronautics (AIAA 2010).
Copyright AIAA.
[.pdf]
- Analyse Statique par Interprétation Abstraite.
Xavier Rival.
In Technique des Sciences Informatiques.
[.pdf]
- Separating Shape Graphs.
Vincent Laviron, Bor-Yuh Evan Chang and Xavier Rival.
In European Symposium On Programming 2010 (ESOP'10).
[.pdf]
- Why does Astrée scale up?
Patrick Cousot, Radhia Cousot, Jérôme Feret,
Laurent Mauborgne, Antoine Miné and Xavier Rival.
In Formal Methods in System Design (FMSD), volume 35(3), pages 229-264, 2009.
[.pdf]
- Space Software Validation using Abstract Interpretation.
Olivier Bouissou, Eric Conquet, Patrick Cousot, Radhia Cousot,
Jérôme Feret, Khalil Ghorbal, Eric Goubault,
David Lesens, Laurent Mauborgne, Antoine Miné, Sylvie Putot,
Xavier Rival and Michel Turin.
In DAta System In Aerospace (DASIA 2009). ESA 2009.
[.pdf]
-
A Static Analyzer for Large Safety-Critical Software.
Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret,
Laurent Mauborgne, Antoine Miné, David Monniaux & Xavier Rival.
In ACM Programming Language Design and Implementation (PLDI 2003).
[.pdf]
- Abstract Interpretation Based Certification
of Assembly Code,
Xavier Rival.
In Proc. 4th International Conference on Verification, Model Checking
and Abstract Interpretation (VMCAI'2003), New York, Jan. 2003
Lecture Notes in Computer Science.
[.pdf]
- Design and Implementation of a Special-Purpose Static
Program Analyzer for Safety-Critical Real-Time Embedded Software, invited chapter.
Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme
Feret, Laurent Mauborgne, Antoine Miné, David Monniaux
and Xavier Rival.
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.
[.pdf]
- Proofnets and Context Semantics for the Additives.
Harry Mairson and Xavier Rival.
In Proc. Computer Science Logic (CSL'02),
Edinburgh, Scotland, Sep. 2002, Lecture Notes in Computer Science. Springer, 2002.
[.pdf]
- Experiments with finite tree automata in Coq.
Xavier Rival and Jean Goubault-Larrecq.
In Proc. 14th Int. Conf. Theorem Proving in Higher Order Logics (TPHOL'01),
Edinburgh, Scotland, Sep. 2001, Lecture Notes in Computer Science. Springer, 2001.
[.pdf]