Search

Your search keyword '"Xavier Rival"' showing total 120 results
Start Over Author "Xavier Rival"
120 results on '"Xavier Rival"'

1. Modular Construction of Shape-Numeric Analyzers

Author

Bor-Yuh Evan Chang and Xavier Rival

Subjects
Mathematics, QA1-939, Electronic computers. Computer science, QA75.5-76.95
Abstract

The aim of static analysis is to infer invariants about programs that are precise enough to establish semantic properties, such as the absence of run-time errors. Broadly speaking, there are two major branches of static analysis for imperative programs. Pointer and shape analyses focus on inferring properties of pointers, dynamically-allocated memory, and recursive data structures, while numeric analyses seek to derive invariants on numeric values. Although simultaneous inference of shape-numeric invariants is often needed, this case is especially challenging and is not particularly well explored. Notably, simultaneous shape-numeric inference raises complex issues in the design of the static analyzer itself. In this paper, we study the construction of such shape-numeric, static analyzers. We set up an abstract interpretation framework that allows us to reason about simultaneous shape-numeric properties by combining shape and numeric abstractions into a modular, expressive abstract domain. Such a modular structure is highly desirable to make its formalization and implementation easier to do and get correct. To achieve this, we choose a concrete semantics that can be abstracted step-by-step, while preserving a high level of expressiveness. The structure of abstract operations (i.e., transfer, join, and comparison) follows the structure of this semantics. The advantage of this construction is to divide the analyzer in modules and functors that implement abstractions of distinct features.

Published
2013
Full Text
View/download PDF

24. Smoothness Analysis for Probabilistic Programs with Application to Optimised Variational Inference

Author

Wonyeol Lee, Xavier Rival, Hongseok Yang, Stanford University, Analyse Statique par Interprétation Abstraite (ANTIQUE), Département d'informatique - ENS Paris (DI-ENS), École normale supérieure - Paris (ENS-PSL), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Paris (ENS-PSL), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria), Department of Computer Science [KAIST] (CS), Korea Advanced Institute of Science and Technology (KAIST), Yang was supported by the Engineering Research Center Program through the National Research Foundation of Korea (NRF) funded by the Korean Government MSIT (NRF-2018R1A5A1059921) and also by the Institute for Basic Science (IBS-R029-C1). Rival was supported by the French ANR VeriAMOS project, and ANR-18-CE25-0010,VeriAMOS,Vérification de Machines Abstraites pour les Systèmes d'Exploitation(2018)

Subjects
FOS: Computer and information sciences, Computer Science - Machine Learning, Computer Science - Programming Languages, Probabilistic programming, [INFO]Computer Science [cs], Safety, Risk, Reliability and Quality, Static analysis, Variational inference, Smoothness, Software, Programming Languages (cs.PL), Machine Learning (cs.LG)
Abstract

We present a static analysis for discovering differentiable or more generally smooth parts of a given probabilistic program, and show how the analysis can be used to improve the pathwise gradient estimator, one of the most popular methods for posterior inference and model learning. Our improvement increases the scope of the estimator from differentiable models to non-differentiable ones without requiring manual intervention of the user; the improved estimator automatically identifies differentiable parts of a given probabilistic program using our static analysis, and applies the pathwise gradient estimator to the identified parts while using a more general but less efficient estimator, called score estimator, for the rest of the program. Our analysis has a surprisingly subtle soundness argument, partly due to the misbehaviours of some target smoothness properties when viewed from the perspective of program analysis designers. For instance, some smoothness properties are not preserved by function composition, and this makes it difficult to analyse sequential composition soundly without heavily sacrificing precision. We formulate five assumptions on a target smoothness property, prove the soundness of our analysis under those assumptions, and show that our leading examples satisfy these assumptions. We also show that by using information from our analysis instantiated for differentiability, our improved gradient estimator satisfies an important differentiability requirement and thus computes the correct estimate on average (i.e., returns an unbiased estimate) under a regularity condition. Our experiments with representative probabilistic programs in the Pyro language show that our static analysis is capable of identifying smooth parts of those programs accurately, and making our improved pathwise gradient estimator exploit all the opportunities for high performance in those programs., Comment: To appear at POPL 2023 (camera-ready version with the appendix)

Published
2023

36. The ASTREÉ Analyzer.

Author

Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival

Published
2005
Full Text
View/download PDF

45. No Crash, No Exploit: Automated Verification of Embedded Kernels

Author

Matthieu Lemerre, Sébastien Bardin, Olivier Nicole, Xavier Rival, Analyse Statique par Interprétation Abstraite (ANTIQUE), Département d'informatique - ENS Paris (DI-ENS), École normale supérieure - Paris (ENS-PSL), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Paris (ENS-PSL), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria), CEA- Saclay (CEA), Commissariat à l'énergie atomique et aux énergies alternatives (CEA), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Université Paris sciences et lettres (PSL), Xavier Rival received funding from the French ANR, as part of the Veriamos grant. Matthieu Lemerre and S ́ebastien Bardin also received funding from the ANR as part of the TAVA grant., and Rival, Xavier

Subjects
FOS: Computer and information sciences, Computer Science - Cryptography and Security, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], Exploit, Operating Systems (cs.OS), Computer science, Crash, computer.file_format, Formal methods, [INFO.INFO-PL] Computer Science [cs]/Programming Languages [cs.PL], Computer Science - Operating Systems, Software bug, Computer engineering, Simple (abstract algebra), Kernel (statistics), Executable, Cryptography and Security (cs.CR), Privilege escalation, computer
Abstract

The kernel is the most safety- and security-critical component of many computer systems, as the most severe bugs lead to complete system crash or exploit. It is thus desirable to guarantee that a kernel is free from these bugs using formal methods, but the high cost and expertise required to do so are deterrent to wide applicability. We propose a method that can verify both absence of runtime errors (i.e. crashes) and absence of privilege escalation (i.e. exploits) in embedded kernels from their binary executables. The method can verify the kernel runtime independently from the application, at the expense of only a few lines of simple annotations. When given a specific application, the method can verify simple kernels without any human intervention. We demonstrate our method on two different use cases: we use our tool to help the development of a new embedded real-time kernel, and we verify an existing industrial real-time kernel executable with no modification. Results show that the method is fast, simple to use, and can prevent real errors and security vulnerabilities., Comment: Published in IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS'21)

Published
2021

46. 08441 Final Report - Emerging Uses and Paradigms for Dynamic Binary Translation.

Author

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 0001, Wei-Chung Hsu, Jens Knoop, Andreas Krall, Naveen Kumar 0002, Jonas Maebe, Robert Muth, Xavier Rival, Erven Rohou, Roni Rosner, Mary Lou Soffa, Jens Tröger, and Christopher A. Vick

Published
2008

47. Weakly sensitive analysis for JavaScript object‐manipulating programs

Author

Sukyoung Ryu, Xavier Rival, and Yoonseok Ko

Subjects
Programming language, Computer science, business.industry, 020207 software engineering, 02 engineering and technology, Static analysis, computer.software_genre, JavaScript, Object (computer science), Call graph, Field (computer science), 0202 electrical engineering, electronic engineering, information engineering, Web application, business, computer, Software, computer.programming_language
Abstract

While JavaScript programs have become pervasive in web applications, they remain hard to reason about. In this context, most static analyses for JavaScript programs require precise call-graph information, since the presence of large numbers of spurious callees significantly deteriorate precision. One of the most challenging JavaScript features that complicate the inference of precise static call graph information is read / write accesses to object fields the names of which are computed at runtime. JavaScript framework libraries often exploit this facility to build objects from other objects, as a way to simulate sophisticated high-level programming constructions. Such code patterns are difficult to analyze precisely, due to weak updates and limitations of unrolling techniques. In this paper, we observe that precise field correspondence relations can be inferred by locally reasoning about object copies, both regarding to the object and to the program structure, and we propose an abstraction which allows to separately reason about field read / write access patterns working on different fields, and to carefully handle the sets of JavaScript object fields. We formalize and implement an analysis based on this technique. We evaluate the performance and precision of the analysis on the computation of call-graph information for examples from jQuery tutorials.

Published
2019

48. A relational shape abstract domain

Author

Matthieu Lemerre, Hugo Illous, Xavier Rival, CEA- Saclay (CEA), Commissariat à l'énergie atomique et aux énergies alternatives (CEA), Analyse Statique par Interprétation Abstraite (ANTIQUE), Département d'informatique - ENS Paris (DI-ENS), École normale supérieure - Paris (ENS-PSL), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Paris (ENS-PSL), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Université Paris sciences et lettres (PSL), Laboratoire Sûreté des Logiciels (LSL), Département Ingénierie Logiciels et Systèmes (DILS), Laboratoire d'Intégration des Systèmes et des Technologies (LIST), Direction de Recherche Technologique (CEA) (DRT (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Direction de Recherche Technologique (CEA) (DRT (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Université Paris-Saclay-Laboratoire d'Intégration des Systèmes et des Technologies (LIST), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Université Paris-Saclay, Département d'informatique de l'École normale supérieure (DI-ENS), École normale supérieure - Paris (ENS Paris), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Paris (ENS Paris), Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Paris (ENS Paris), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Paris (ENS Paris), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Inria de Paris, Laboratoire d'Intégration des Systèmes et des Technologies (LIST (CEA)), and Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Université Paris-Saclay-Laboratoire d'Intégration des Systèmes et des Technologies (LIST (CEA))

Subjects
Theoretical computer science, Computer science, Separation Logic, 0102 computer and information sciences, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], 02 engineering and technology, Separation logic, 01 natural sciences, Logical connective, Theoretical Computer Science, Domain (software engineering), Set (abstract data type), 0202 electrical engineering, electronic engineering, information engineering, Relational properties, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], business.industry, 020208 electrical & electronic engineering, 020207 software engineering, Abstract interpretation, Semantic property, Static analysis, Modular design, Shape analysis, 010201 computation theory & mathematics, Hardware and Architecture, State (computer science), business, Software
Abstract

International audience; Static analyses aim at inferring semantic properties of programs. We distinguish two important classes of static analyses: state analyses and relational analyses. While state analyses aim at computing an over-approximation of reachable states of programs, relational analyses aim at computing functional properties over the input-output states of programs. Several advantages of relational analyses are their ability to analyze incomplete programs, such as libraries or classes, but also to make the analysis modular, using input-output relations as composable summaries for procedures. In the case of numerical programs, several analyses have been proposed that utilize relational numerical abstract domains to describe relations. On the other hand, designing abstractions for relations over input-output memory states and taking shapes into account is challenging. In this paper, we propose a set of novel logical connectives to describe such relations, which are inspired by separation logic. This logic can express that certain memory areas are unchanged, freshly allocated, or freed, or that only part of the memory was modified. Using these connectives, we build an abstract domain and design a static analysis that over-approximates relations over memory states containing inductive structures. We implement this analysis and report on the analysis of basic libraries of programs manipulating lists and trees.

Published
2021

49. Shape Analysis

Author

Xavier Rival, Noam Rinetzky, Roman Manevich, Cezara Drăgoi, and Bor-Yuh Evan Chang

Published
2020

50. Interprocedural Shape Analysis Using Separation Logic-Based Transformer Summaries

Author

Xavier Rival, Matthieu Lemerre, Hugo Illous, Rival, Xavier, APPEL À PROJETS GÉNÉRIQUE 2018 - Vérification de Machines Abstraites pour les Systèmes d'Exploitation - - VeriAMOS2018 - ANR-18-CE25-0010 - AAPG2018 - VALID, Commissariat à l'énergie atomique et aux énergies alternatives (CEA), Analyse Statique par Interprétation Abstraite (ANTIQUE), Département d'informatique - ENS Paris (DI-ENS), Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Paris (ENS Paris), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Paris (ENS Paris), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL), This work has r ceived support from the French ANR as part of the VeriAMOS grant., ANR-18-CE25-0010,VeriAMOS,Vérification de Machines Abstraites pour les Systèmes d'Exploitation(2018), École normale supérieure - Paris (ENS-PSL), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Paris (ENS-PSL), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Inria de Paris, Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Département d'informatique de l'École normale supérieure (DI-ENS), École normale supérieure - Paris (ENS Paris), and Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Paris (ENS Paris)

Subjects
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], Shape analysis (program analysis), Programming language, Computer science, business.industry, 0102 computer and information sciences, 02 engineering and technology, Separation logic, [INFO] Computer Science [cs], Modular design, computer.software_genre, 01 natural sciences, [INFO.INFO-PL] Computer Science [cs]/Programming Languages [cs.PL], Set (abstract data type), Transformation (function), 010201 computation theory & mathematics, 0202 electrical engineering, electronic engineering, information engineering, [INFO]Computer Science [cs], 020201 artificial intelligence & image processing, Abstraction, State (computer science), business, computer, Transformer (machine learning model)
Abstract

International audience; Shape analyses aim at inferring semantic invariants related to the data-structures that programs manipulate. To achieve that, they typically abstract the set of reachable states. By contrast, abstractions for transformation relations between input states and output states not only provide a finer description of program executions but also enable the composition of the effect of program fragments so as to make the analysis modular. However, few logics can efficiently capture such transformation relations. In this paper, we propose to use connectors inspired by separation logic to describe memory state transformations and to represent procedure summaries. Based on this abstraction, we design a top-down interprocedural analysis using shape transformation relations as procedure summaries. Finally, we report on implementation and evaluation.

Published
2020

Catalog

Books, media, physical & digital resources
See catalog results