Demo Data from EDBT 2026 / reviewers in the wild / expert
Antoine Rauzy
dblp:r/AntoineRauzy · also Antoine B. Rauzy
· DBLP profile ↗
22ranked-venue papers
8as first author
1since 2021 · last 2023
0000-0003-0926-5286ORCID · verified
Domains — the database's venue-derived domains; a paper can count in several
Software engineering, systems software and programming languages · 7 · 3 first-authorTheory of computation · 7 · 2 first-authorApplied, interdisciplinary, general and emerging computing · 7 · 4 first-author · 1 since 2021Artificial intelligence and machine learning · 6 · 2 first-authorSystems, architecture and hardware · 1Databases, data management, data science and information retrieval · 1
Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.
| Theoretical computer science
1 paper |
Logic in computer science · 100% |
Topics — the 2 heaviest of 2, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Logic in computer science › logic programming
constraint logic programming |
0.0 | 1 | 1995 | Toupie = µ-Calculus + Constraints · CAV 1995 |
Logic in computer science › modal logic › multi-modal logic
modal mu-calculus |
0.0 | 1 | 1995 | Toupie = µ-Calculus + Constraints · CAV 1995 |
Methods — techniques the papers use, named apart from their topics
mu-calculus · 0.0constraint solving · 0.0
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2023 | Minimal Critical Sequences in Model-based Safety and Security Analyses: Commonalities and DifferencesabstractDiscrete event systems are increasingly used as a modeling tool to assess safety and cybersecurity of complex systems. In both cases, the analysis relies on the extraction of critical sequences. This approach proves to be very powerful. It suffers, however, from the combinatorial explosion of the number of sequences to look at. To push the limits of what is feasible with reasonable computational resources, extraction algorithms use cutoffs and minimality criteria. In this article, we review the principles of extraction algorithms, and we show that there are important differences between critical sequences extracted in the context of safety analyses and those extracted in the context of cybersecurity analyses. Based on this thorough comparison, we introduce a new cutoff criterion, so-called footprint, that aims at capturing the willfulness of an intruder performing a cyberattack. We illustrate our presentation by means of three case studies, one focused on the analysis of failures and two focused on the analysis of cyberattacks and their effects on safety. We show experimentally the interest of the footprint criterion. Théo Serru, Nga Nguyen 0001, Michel Batteux, Antoine Rauzy |
ACM Trans. Cyber Phys. Syst. | 4 |
| 2013 | The AltaRica 3.0 project for model-based safety assessmentabstract“Traditional” risk modeling formalisms (e.g. FMEA, Fault Trees, Markov Processes, etc.) are well mastered by safety analysts. Efficient algorithms and tools are available. However, models designed with these formalisms are far from the specifications of the systems under study. They are consequently hard to design and to maintain throughout the life cycle of systems. The high-level modeling language AltaRica has been created to tackle this problem. The objective of the AltaRica 3.0 project is to design a new version of AltaRica, and to develop a complete set of authoring, simulation and assessment tools to perform safety analyses: virtual experiments on systems, via models, calculation of different kinds of reliability indicators, etc. AltaRica 3.0 improves significantly the expressive power of AltaRica Data-Flow without decreasing the efficiency of its assessment algorithms. Prototypes of a Fault Tree compiler, a stochastic and a stepwise simulators have been already developed. Other tools are under specification or implementation. Michel Batteux, Tatiana Prosvirnova, Antoine Rauzy, Leïla Kloul |
INDIN | 3 |
| 2008 | Efficient Reliability Assessment of Redundant Systems Subject to Imperfect Fault Coverage Using Binary Decision DiagramsabstractSystems requiring very high levels of reliability, such as aircraft controls or spacecraft, often use redundancy to achieve their requirements. This paper provides highly efficient techniques for computing the reliability of redundant systems involving simplek-out-of-narrangements, and those involving complex structures which may include imbeddedk-out-of-nstructures. Techniques for modeling systems subject to imperfect fault coverage must be appropriate to the redundancy management architecture utilized by the system. Systems for which coverage can be associated with each of the redundant components, perhaps taking advantage of the component's built-in test capability, are modeled with what we term element level coverage (ELC); while systems which utilize majority voting for the selection from among redundant components are modeled with fault level coverage (FLC). In FLC, systems coverage is a function of the fault sequence, i.e., coverage will be greater for the initial faults which can utilize voting for redundant component selection, but will have a lower coverage value when the system must select from among the last two operational components. Occasionally, FLC systems can be adequately modeled using a simplified version of FLC in which it can be assumed that the initial fault coverage values are unity. This model is called one-on-level coverage (OLC). The FLC algorithms provided in this paper are of particular importance for the correct modeling of systems which utilize voting to select from among their redundant elements. While combinatorial, and recursive techniques for modeling ELC, FLC, and OLC have been previously reported, this paper presents new table-based algorithms, and binary decision diagram-based algorithms for these models which have superior computational complexity. The algorithms presented here provide the ability to analyse large, and complex systems very efficiently, in fact with a computational complexity comparable to the best available techniques for systems with perfect fault coverage. Albert F. Myers, Antoine Rauzy |
IEEE Trans. Reliab. | 2 |
| 2005 | A m log m algorithm to compute the most probable configurations of a system with multi-mode independent componentsabstractIn this note, we propose a m log m algorithm to find the k most probable configurations of a system of n multi-mode independent components, with at most d modes each. m denotes the size of the problem, i.e. max (nd, k). This problem originates in network performance analyzes, in which focusing on the most probable configurations is a means to reduce computational costs. Up to this note, the best known algorithm to extract the most probable configurations was in O(n/sup 2/d/sup 2/ + k log k). Our algorithm achieves thus a substantial improvement. Antoine Rauzy |
IEEE Trans. Reliab. | 1 |
| 2003 | A new methodology to handle Boolean models with loopsabstractIt is often convenient, in reliability analyses, to describe the system under study by means of a set of Boolean equations. Fault trees can be seen as hierarchical sets of Boolean equations. In some cases, the model contains loops, because the system embeds at least two components whose states depend on one another. Reliability networks are a typical example of looped models. Classical fault tree assessment methods fail to assess this kind of model. This paper proposes a logical framework to clarify the meaning of looped sets of Boolean equations; and a binary decision diagrams based method is proposed to assess them. This approach is illustrated with experimental results on a benchmark of reliability networks. Antoine Rauzy |
IEEE Trans. Reliab. | 1 |
| 2003 | Toward an efficient implementation of the MOCUS algorithmabstractMOCUS is probably the most famous algorithm to compute minimal cutsets of fault trees. It was proposed by Fussell and Vesely in 1972. It is now the core method of many fault-tree assessment tools. Despite its wide use, textbooks and articles give very few details about how to implement it. This paper describes data structures as well as several improvements and heuristics that make MOCUS very efficient. Experiments on a benchmark of the 1819 event-tree sequences that were generated during a PSA study are reported. Advantages and drawbacks of MOCUS and Binary Decision Diagrams are discussed. Antoine Rauzy |
IEEE Trans. Reliab. | 1 |
| 2001 | A realistic involvement of formal methodsabstractIn this article, we report a real-life application of so-called ‘Formal Methods’. The part of the project we were involved in was to verify that an embedded circuit satisfies a safety property. We describe the circuit as well as the mathematical and computer tools we used. We discuss methodological issues and we present some of the various experiments we performed. Finally, we draw some general conclusions about the practicability of formal verification techniques. Copyright © 2001 John Wiley & Sons, Ltd. Didier Bégay, Antoine Rauzy |
Softw. Pract. Exp. | 2 |
| 2001 | Mathematical foundations of minimal cutsetsabstractSince their introduction in the reliability field, binary decision diagrams have proved to be the most efficient tool to assess Boolean models such as fault trees. Their success increases the need of sound mathematical foundations for the notions that are involved in reliability and dependability studies. This paper clarifies the mathematical status of the notion of minimal cutsets which have a central role in fault-tree assessment. Algorithmic issues are discussed. Minimal cutsets are distinct from prime implicants and they have a great interest from both a computation complexity and practical viewpoint. Implementation of BDD algorithms is explained. All of these algorithms are implemented in the Aralia software, which is widely used. These algorithms and their mathematical foundations were designed to assess efficiently a very large noncoherent fault tree that models the emergency shutdown system of a nuclear reactor. Antoine Rauzy |
IEEE Trans. Reliab. | 1 |
| 2000 | Bypassing BDD construction for reliability analysis
Poul Frederick Williams, Macha Nikolskaïa, Antoine Rauzy |
Inf. Process. Lett. | 3 |
| 1999 | The AltaRica Formalism for Describing Concurrent SystemsabstractThe AltaRica formalism is designed for describing complex systems consisting of a number of interacting components. Its semantics is expressed in terms of transition systems so that a system described in this language can be analysed by any technique or tool applicable to transition systems. The components of a system have two kinds of interactions • event synchronisation, like in the synchronized product of transition systems of Arnold and Nivat, • interface coordination: with each component are associated interfaces whose values depend on the state of the component as well as on the values of interfaces of other components of the system. Another feature of AltaRica is the possibility of defining hierarchical systems: some subsystems can be encapsulated and their mutual interactions as well as their interactions with the rest of the system are supervised by a controller. André Arnold, Gérald Point, Alain Griffault, Antoine Rauzy |
Fundam. Informaticae | 4 |
| 1998 | Almana: A BDD Minimization Tool Integrating Heuristic and Rewriting Methods
Macha Nikolskaïa, Antoine Rauzy, David J. Sherman |
FMCAD | 2 |
| 1997 | Toupie: The µ-calculus over Finite Domains as a Constraint Language
Marc-Michel Corsini, Antoine Rauzy |
J. Autom. Reason. | 2 |
| 1996 | A linear-time algorithm to find modules of fault treesabstractA module of a fault tree is a subtree whose terminal events do not occur elsewhere in the tree. Modules, which are independent subtrees, can be used to reduce the computational cost of basic operations on fault trees, such as the computation of the probability of the root event or the computation of the minimal cut sets. This paper presents a linear time algorithm to detect modules of a fault tree, coherent or not, that is derived from the Tarjan algorithm to find strongly connected components of a graph. The authors show, on a benchmark of real fault trees, that their method detects modules of trees with several hundred gates and events within few milliseconds on a personal computer. Yves Dutuit, Antoine Rauzy |
IEEE Trans. Reliab. | 2 |
| 1995 | Toupie = µ-Calculus + Constraints
Antoine Rauzy |
CAV | 1 |
| 1995 | Polynomial Restrictions of SAT: What Can Be Done with an Efficient Implementation of the Davis and Putnam's Procedure?
Antoine Rauzy |
CP | 1 |
| 1995 | Revision in Extended Propositional Calculus
Odile Papini, Antoine Rauzy |
ECSQARU | 2 |
| 1994 | Symbolic Model Checking and Constraint Logic Programming: a Cross-Fertilization
Marc-Michel Corsini, Antoine Rauzy |
ESOP | 2 |
| 1994 | Notes on the Design of an Open Boolean Solver
Antoine Rauzy |
ICLP | 1 |
| 1993 | A Mixed Approach of Revision in Propositional Calculus
Odile Papini, Antoine Rauzy |
ECSQARU | 2 |
| 1993 | Safety Analysis by Means of Fault Trees: An Application for Open Boolean Solvers
Marc-Michel Corsini, Antoine Rauzy |
ICLP | 2 |
| 1993 | Yet Another Application for Topie: Verification of Mutual Exclusion Algorithms
Marc-Michel Corsini, Alain Griffault, Antoine Rauzy |
LPAR | 3 |
| 1991 | Knowledge Extraction in Trivalued Propositional Logic
Antoine Rauzy |
ECSQARU | 1 |