Xavier Rival

75 papers A* 6A 6B 22Misc 1Journal 27Unranked 10
YearRankTypeTitle / Venue / Authors
2026 J jnl
Optimising Density Computations in Probabilistic Programs via Automatic Loop Vectorisation.
Proc. ACM Program. Lang.
Sangho Lim, Hyoungjin Lim, Wonyeol Lee, Xavier Rival, Hongseok Yang
2025 J jnl
Optimising Density Computations in Probabilistic Programs via Automatic Loop Vectorisation.
CoRR
Sangho Lim, Hyoungjin Lim, Wonyeol Lee, Xavier Rival, Hongseok Yang
2023 B conf
A Categorical Framework for Program Semantics and Semantic Abstraction.
MFPS
Shin-ya Katsumata, Xavier Rival, Jérémy Dubut
2023 B conf
A Product of Shape and Sequence Abstractions.
SAS
Josselin Giet, Félix Ridoux, Xavier Rival
2023 J jnl
Smoothness Analysis for Probabilistic Programs with Application to Optimised Variational Inference.
Proc. ACM Program. Lang.
Wonyeol Lee, Xavier Rival, Hongseok Yang
2023 B conf
Sound Symbolic Execution via Abstract Interpretation and Its Application to Security.
VMCAI
Ignacio Tiraboschi, Tamara Rezk, Xavier Rival
2023 J jnl
Sound Symbolic Execution via Abstract Interpretation and its Application to Security.
CoRR
Ignacio Tiraboschi, Tamara Rezk, Xavier Rival
2022 B conf
Lightweight Shape Analysis Based on Physical Types.
VMCAI
Olivier Nicole, Matthieu Lemerre, Xavier Rival
2022 J jnl
Smoothness Analysis for Probabilistic Programs with Application to Optimised Variational Inference.
CoRR
Wonyeol Lee, Xavier Rival, Hongseok Yang
2021 J jnl
A relational shape abstract domain.
Formal Methods Syst. Des.
Hugo Illous, Matthieu Lemerre, Xavier Rival
2021 A conf
No Crash, No Exploit: Automated Verification of Embedded Kernels.
RTAS
Olivier Nicole, Matthieu Lemerre, Sébastien Bardin, Xavier Rival
2020 J jnl
Automatically Proving Microkernels Free from Privilege Escalation from their Executable.
CoRR
Olivier Nicole, Matthieu Lemerre, Sébastien Bardin, Xavier Rival
2020 B conf
Interprocedural Shape Analysis Using Separation Logic-Based Transformer Summaries.
SAS
Hugo Illous, Matthieu Lemerre, Xavier Rival
2020 J jnl
No Crash, No Exploit: Automated Verification of Embedded Kernels.
CoRR
Olivier Nicole, Matthieu Lemerre, Sébastien Bardin, Xavier Rival
2020 A* conf
On Correctness of Automatic Differentiation for Non-Differentiable Functions.
NeurIPS
Wonyeol Lee, Hangyeol Yu, Xavier Rival, Hongseok Yang
2020 J jnl
On Correctness of Automatic Differentiation for Non-Differentiable Functions.
CoRR
Wonyeol Lee, Hangyeol Yu, Xavier Rival, Hongseok Yang
2020 J jnl
Shape Analysis.
Found. Trends Program. Lang.
Bor-Yuh Evan Chang, Cezara Dragoi, Roman Manevich, Noam Rinetzky, Xavier Rival
2020 J jnl
Towards verified stochastic variational inference for probabilistic programs.
Proc. ACM Program. Lang.
Wonyeol Lee, Hangyeol Yu, Xavier Rival, Hongseok Yang
2019 J jnl
Towards Verified Stochastic Variational Inference for Probabilistic Programs.
CoRR
Wonyeol Lee, Hangyeol Yu, Xavier Rival, Hongseok Yang
2019 J jnl
Weakly sensitive analysis for JavaScript object-manipulating programs.
Softw. Pract. Exp.
Yoonseok Ko, Xavier Rival, Sukyoung Ryu
2018 J jnl
A Theoretical Foundation of Sensitivity in an Abstract Interpretation Framework.
ACM Trans. Program. Lang. Syst.
Se-Won Kim, Xavier Rival, Sukyoung Ryu
2018 J jnl
Automatic Verification of Embedded System Code Manipulating Dynamic Structures Stored in Contiguous Regions.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.
Jiangchao Liu, Liqian Chen, Xavier Rival
2018 J jnl
Foreword.
Formal Methods Syst. Des.
Xavier Rival
2017 — conf
A Relational Shape Abstract Domain.
NFM
Hugo Illous, Matthieu Lemerre, Xavier Rival
2017 J jnl
An array content static analysis based on non-contiguous partitions.
Comput. Lang. Syst. Struct.
Jiangchao Liu, Xavier Rival
2017 J jnl
Memory Abstraction, Emerging Techniques and Applications (NII Shonan Meeting 2017-12).
NII Shonan Meet. Rep.
Bor-Yuh Evan Chang, Xavier Rival, Sukyoung Ryu
2017 — conf
Revisiting recency abstraction for JavaScript: towards an intuitive, compositional, and efficient heap abstraction.
SOAP@PLDI
Jihyeok Park, Xavier Rival, Sukyoung Ryu
2017 A* conf
Semantic-directed clumping of disjunctive abstract states.
POPL
Huisong Li, Francois Berenger, Bor-Yuh Evan Chang, Xavier Rival
2017 B conf
Weakly Sensitive Analysis for Unbounded Iteration over JavaScript Objects.
APLAS
Yoonseok Ko, Xavier Rival, Sukyoung Ryu
2016 — ed.
Proceedings of the 5th ACM SIGPLAN International Workshop on State Of the Art in Program Analysis, SOAP@PLDI 2016, Santa Barbara, CA, USA, June 14, 2016
SOAP@PLDI
Charles Zhang, Xavier Rival
2016 B ed.
Static Analysis - 23rd International Symposium, SAS 2016, Edinburgh, UK, September 8-10, 2016, Proceedings
SAS
Xavier Rival
2015 B conf
Abstract Domains and Solvers for Sets Reasoning.
LPAR
Arlen Cox, Bor-Yuh Evan Chang, Huisong Li, Xavier Rival
2015 B conf
Abstraction of Arrays Based on Non Contiguous Partitions.
VMCAI
Jiangchao Liu, Xavier Rival
2015 B conf
Abstraction of Optional Numerical Values.
APLAS
Jiangchao Liu, Xavier Rival
2015 A conf
Desynchronized Multi-State Abstractions for Open Programs in Dynamic Languages.
ESOP
Arlen Cox, Bor-Yuh Evan Chang, Xavier Rival
2015 B conf
Shape Analysis for Unstructured Sharing.
SAS
Huisong Li, Xavier Rival, Bor-Yuh Evan Chang
2015 J jnl
Static Analysis and Verification of Aerospace Software by Abstract Interpretation.
Found. Trends Program. Lang.
Julien Bertrane, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, Xavier Rival
2015 A conf
Static Analysis of Spreadsheet Applications for Type-Unsafe Operations Detection.
ESOP
Tie Cheng, Xavier Rival
2015 J jnl
Synthesizing Short-Circuiting Validation of Data Structure Invariants.
CoRR
Yi-Fan Tsai, Devin Coughlin, Bor-Yuh Evan Chang, Xavier Rival
2014 B conf
An Abstract Domain Combinator for Separately Conjoining Memory Abstractions.
SAS
Antoine Toubhans, Bor-Yuh Evan Chang, Xavier Rival
2014 B conf
Automatic Analysis of Open Objects in Dynamic Language Programs.
SAS
Arlen Cox, Bor-Yuh Evan Chang, Xavier Rival
2014 — conf
Construction of Abstract Domains for Heterogeneous Properties (Position Paper).
ISoLA (2)
Xavier Rival, Antoine Toubhans, Bor-Yuh Evan Chang
2014 B ed.
Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014, San Diego, CA, USA, January 19-21, 2014, Proceedings
VMCAI
Kenneth L. McMillan, Xavier Rival
2013 — conf
Modular Construction of Shape-Numeric Analyzers.
Festschrift for Dave Schmidt
Bor-Yuh Evan Chang, Xavier Rival
2013 B conf
Reduced Product Combination of Abstract Domains for Shapes.
VMCAI
Antoine Toubhans, Bor-Yuh Evan Chang, Xavier Rival
2012 B conf
An Abstract Domain to Infer Types over Zones in Spreadsheets.
SAS
Tie Cheng, Xavier Rival
2012 B conf
Hierarchical Shape Abstraction of Dynamic Structures in Static Blocks.
APLAS
Pascal Sotin, Xavier Rival
2011 J jnl
Analyse statique par interprétation abstraite.
Tech. Sci. Informatiques
Xavier Rival
2011 A* conf
Calling context abstraction with shapes.
POPL
Xavier Rival, Bor-Yuh Evan Chang
2011 J jnl
Static analysis by abstract interpretation of embedded critical software.
ACM SIGSOFT Softw. Eng. Notes
Julien Bertrane, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, Xavier Rival
2010 — conf
Concrete Memory Models for Shape Analysis.
NSAD@SAS
Pascal Sotin, Bertrand Jeannet, Xavier Rival
2010 — conf
Preface.
TAPAS@SAS
David Delmas, Xavier Rival
2010 — ed.
Proceedings of the Tools for Automatic Program AnalysiS, TAPAS@SAS 2010, Perpignan, France, September 17, 2010
TAPAS@SAS
David Delmas, Xavier Rival
2010 A conf
Separating Shape Graphs.
ESOP
Vincent Laviron, Bor-Yuh Evan Chang, Xavier Rival
2009 J jnl
Astree: Nachweis der Abwesenheit von Laufzeit.
Softwaretechnik-Trends
Daniel Kästner, Christian Ferdinand, Stephan Wilhelm, Stefana Nenova, Olha Honcharova, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, Xavier Rival, Élodie-Jane Sims
2009 J jnl
Why does Astrée scale up?
Formal Methods Syst. Des.
Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, Xavier Rival
2008 — conf
08441 Final Report - Emerging Uses and Paradigms for Dynamic Binary Translation.
Emerging Uses and Paradigms for Dynamic Binary Translation
Erik R. Altman, Bruce R. Childers, Robert S. Cohn, Jack W. Davidson, Koen De Bosschere, Bjorn De Sutter, M. Anton Ertl, Michael Franz, Yuan Xiang Gu, Matthias Hauswirth, Thomas Heinz, Wei-Chung Hsu, Jens Knoop, Andreas Krall, Naveen Kumar, Jonas Maebe, Robert Muth, Xavier Rival, Erven Rohou, Roni Rosner, Mary Lou Soffa, Jens Tröger, Christopher A. Vick
2008 A* conf
Relational inductive shape analysis.
POPL
Bor-Yuh Evan Chang, Xavier Rival
2007 J jnl
A Static Analyzer for Large Safety-Critical Software
CoRR
Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, Xavier Rival
2007 B conf
Shape Analysis with Structural Invariant Checkers.
SAS
Bor-Yuh Evan Chang, Xavier Rival, George C. Necula
2007 J jnl
The trace partitioning abstract domain.
ACM Trans. Program. Lang. Syst.
Xavier Rival, Laurent Mauborgne
2007 Misc conf
Varieties of Static Analyzers: A Comparison with ASTREE.
TASE
Patrick Cousot, Radhia Cousot, Jérôme Feret, Antoine Miné, Laurent Mauborgne, David Monniaux, Xavier Rival
2006 — conf
Combination of Abstractions in the ASTRÉE Static Analyzer.
ASIAN
Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, Xavier Rival
2005 B conf
Abstract Dependences for Alarm Diagnosis.
APLAS
Xavier Rival
2005 — —
Abstraction de traces en analyse statique et transformation de programmes. (Traces abstraction in static analysis and program transformation).
Xavier Rival
2005 A conf
The ASTREÉ Analyzer.
ESOP
Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, Xavier Rival
2005 A conf
Trace Partitioning in Abstract Interpretation Based Static Analyzers.
ESOP
Laurent Mauborgne, Xavier Rival
2005 B conf
Understanding the Origin of Alarms in Astrée.
SAS
Xavier Rival
2004 J jnl
Certification of compiled assembly code by invariant translation.
Int. J. Softw. Tools Technol. Transf.
Xavier Rival
2004 A* conf
Symbolic transfer function-based approaches to certified compilation.
POPL
Xavier Rival
2003 A* conf
A static analyzer for large safety-critical software.
PLDI
Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, Xavier Rival
2003 B conf
Abstract Interpretation-Based Certification of Assembly Code.
VMCAI
Xavier Rival
2002 — conf
Design and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded Software.
The Essence of Computation
Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, Xavier Rival
2002 B conf
Proofnets and Context Semantics for the Additives.
CSL
Harry G. Mairson, Xavier Rival
2001 — conf
Experiments with Finite Tree Automata in Coq.
TPHOLs
Xavier Rival, Jean Goubault-Larrecq