VLDB 2026 Research / reviewers in the wild / expert
Philippe Quéinnec
dblp:83/6412
· DBLP profile ↗
20ranked-venue papers
3as first author
4since 2021 · last 2023
—ORCID · none
Domains — the database's venue-derived domains; a paper can count in several
Software engineering, systems software and programming languages · 4 · 1 since 2021Theory of computation · 3 · 2 since 2021Systems, architecture and hardware · 2 · 1 first-authorComputer networks · 1Security and privacy · 1Databases, data management, data science and information retrieval · 1 · 1 since 2021Graphics, computer vision, multimedia, augmented reality and games · 1
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2023 | Tasks in modular proofs of concurrent algorithms
Armando Castañeda, Aurélie Hurault, Philippe Quéinnec, Matthieu Roy |
Inf. Comput. | 3 |
| 2022 | A First-Order Logic verification framework for communication-parametric and time-aware BPMN collaborations
Sara Houhou, Souheib Baarir, Pascal Poizat, Philippe Quéinnec, Laid Kahloul |
Inf. Syst. | 4 |
| 2021 | A Direct Formal Semantics for BPMN Time-related ConstructsabstractInternational audience Sara Houhou, Souheib Baarir, Pascal Poizat, Philippe Quéinnec |
ENASE | 4 |
| 2021 | Characterization and Derivation of Heard-Of Predicates for Asynchronous Message-Passing ModelsabstractIn distributed computing, multiple processes interact to solve a problem together. The main model of interaction is the message-passing model, where processes communicate by exchanging messages. Nevertheless, there are several models varying along important dimensions: degree of synchrony, kinds of faults, number of faults... This variety is compounded by the lack of a general formalism in which to abstract these models. One way to bring order is to constrain these models to communicate in rounds. This is the setting of the Heard-Of model, which captures many models through predicates on the messages sent in a round and received on time. Yet, it is not easy to define the predicate that captures a given operational model. The question is even harder for the asynchronous case, as unbounded message delay means the implementation of rounds must depend on details of the model. This paper shows that characterising asynchronous models by heard-of predicates is indeed meaningful. This characterization relies on delivered predicates, an intermediate abstraction between the informal operational model and the heard-of predicates. Our approach splits the problem into two steps: first extract the delivered model capturing the informal model, and then characterize the heard-of predicates that are generated by this delivered model. For the first part, we provide examples of delivered predicates, and an approach to derive more. It uses the intuition that complex models are a composition of simpler models. We define operations like union, succession or repetition that make it easier to derive complex delivered predicates from simple ones while retaining expressivity. For the second part, we formalize and study strategies for when to change rounds. Intuitively, the characterizing predicate of a model is the one generated by a strategy that waits for as much messages as possible, without blocking forever. Adam Shimi, Aurélie Hurault, Philippe Quéinnec |
Log. Methods Comput. Sci. | 3 |
| 2020 | Derivation of Heard-of Predicates from Elementary Behavioral Patterns
Adam Shimi, Aurélie Hurault, Philippe Quéinnec |
FORTE | 3 |
| 2019 | A First-Order Logic Semantics for Communication-Parametric BPMN Collaborations
Sara Houhou, Souheib Baarir, Pascal Poizat, Philippe Quéinnec |
BPM | 4 |
| 2019 | Tasks in Modular Proofs of Concurrent Algorithms
Armando Castañeda, Aurélie Hurault, Philippe Quéinnec, Matthieu Roy |
SSS | 3 |
| 2019 | A modular framework for verifying versatile distributed systems
Florent Chevrou, Aurélie Hurault, Philippe Quéinnec |
J. Log. Algebraic Methods Program. | 3 |
| 2018 | Characterizing Asynchronous Message-Passing Models Through RoundsabstractMessage-passing models of distributed computing vary along numerous dimensions: degree of synchrony, kind of faults, number of faults... Unfortunately, the sheer number of models and their subtle distinctions hinder our ability to design a general theory of message-passing models. One way out of this conundrum restricts communication to proceed by round. A great variety of message-passing models can then be captured in the Heard-Of model, through predicates on the messages sent in a round and received during or before this round. Then, the issue is to find the most accurate Heard-Of predicate to capture a given model. This is straightforward in synchronous models, because waiting for the upper bound on communication delay ensures that all available messages are received, while not waiting forever. On the other hand, asynchrony allows unbounded message delays. Is there nonetheless a meaningful characterization of asynchronous models by a Heard-Of predicate? We formalize this characterization by introducing Delivered collections: the collections of all messages delivered at each round, whether late or not. Predicates on Delivered collections capture message-passing models. The question is to determine which Heard-Of predicates can be generated by a given Delivered predicate. We answer this by formalizing strategies for when to change round. Thanks to a partial order on these strategies, we also find the "best" strategy for multiple models, where "best" intuitively means it waits for as many messages as possible while not waiting forever. Finally, a strategy for changing round that never blocks a process forever implements a Heard-Of predicate. This allows us to translate the order on strategies into an order on Heard-Of predicates. The characterizing predicate for a model is then the greatest element for that order, if it exists. Adam Shimi, Aurélie Hurault, Philippe Quéinnec |
OPODIS | 3 |
| 2017 | Asynchronous Message Orderings Beyond CausalityabstractIn the asynchronous setting, distributed behavior is traditionally studied through computa- tions, the Happened-Before posets of events generated by the system. An equivalent perspective considers the linear extensions of the generated computations: each linear extension defines a sequence of events, called an execution. Both perspective were leveraged in the study of asyn- chronous point-to-point message orderings over computations; yet neither allows us to interpret message orderings defined over executions. Can we nevertheless make sense of such an ordering, maybe even use it to understand asynchronicity better? We provide a general answer by defining a topology on the set of executions which captures the fundamental assumptions of asynchronicity. This topology links each message ordering over executions with two sets of computations: its closure, the computations for which at least one linear extension satisfies the predicate; and its interior, the computations for which all linear ex- tensions satisfy it. These sets of computations represent respectively the uncertainty brought by asynchronicity – the computations where the predicate is satisfiable – and the certainty available despite asynchronicity – the computations where the predicate must hold. The paper demon- strates the use of this topological approach by examining closures and interiors of interesting orderings over executions. Adam Shimi, Aurélie Hurault, Philippe Quéinnec |
OPODIS | 3 |
| 2016 | On the diversity of asynchronous communicationabstractAbstract Asynchronous communication is often viewed as a single entity, the counterpart of synchronous communication. Although the basic concept of asynchronous communication is the decoupling of send and receive events, there is actually room for a variety of additional specification of the communication, for instance in terms of ordering. Yet, these different asynchronous communications are used interchangeably and seldom distinguished. This paper is a contribution to the study of these models, their differences, and how they are related. In this paper, the variety of point-to-point asynchronous communication paradigms is considered with two approaches. In the first and theoretical one, communication models are specified as properties on the ordering of events in distributed executions. In the second and more practical approach that involves composition of peers, they are modeled with transition systems and message histories as part of a framework. The described framework enables to model peer composition and compatibility properties. Besides, an implemented tool chain based on the TLA + formalism and model checking is also proposed and illustrated. The conformance of the two approaches is highlighted. A hierarchy is established between the studied communication models. From the execution viewpoint, it completes existing work in the area by introducing more asynchronous communication models and showing their differences. The framework is shown to offer abstract implementations of the communication models. Both the correctness and the completeness of the descriptions in the framework are studied. This reveals necessary restrictions on the behavior of the peers so that the communication models are actually implementable. Florent Chevrou, Aurélie Hurault, Philippe Quéinnec |
Formal Aspects Comput. | 3 |
| 2013 | Analysis of distributed multiperiodic systems to achieve consistent data matchingabstractSUMMARY The distributed real‐time architecture of an embedded system is often described as a set of communicating components. Such a system is dataflow (for its description) and time triggered (for its execution). The architecture forms a graph of communicating components, where more than one path can link two components. Because the characteristics of the network and the behavior of intermediate components may vary or are only partially known, these paths often have different timing characteristics, and the flows of information that transit on these paths reach their destination at independent times. However, an application that seeks consistent values will require these flows to be temporally matched so that a component uses inputs that all (directly or indirectly) depend on the same computation step of another component. In this paper, we define this temporal data‐matching property, both in a strict sense and in a relaxed way allowing approximately consistent values. Then, we show how to analyze a system architecture to detect situations that result in data‐matching inconsistencies. In the context of multiperiodic systems, where components do not necessarily share a common period, we also describe an approach to manage data matching that uses queues to delay too fast paths and timestamps to recognize consistent data sets. Copyright © 2012 John Wiley & Sons, Ltd. Nadège Pontisso, Philippe Quéinnec, Gérard Padiou |
Concurr. Comput. Pract. Exp. | 2 |
| 2007 | Separability to Help Parallel Simulation of Distributed Computations
Philippe Mauran, Gérard Padiou, Philippe Quéinnec |
OPODIS | 3 |
| 2006 | A Coordination-Level Middleware for Supporting Flexible Consistency in CSCWabstractHighly interactive collaborative applications need to offer each user a consistent view of the interactions represented by the streams exchanged between dispersed groups of users. At the coordination level, strong ordering protocols for capturing and delivering streams' interactions (e.g. CAUSAL, TOTAL order) may be too expensive due to the variability of the network conditions. This paper builds upon previous work on expressing streams causality and proposes a flexible coordination middleware in order to integrate different delivery modes (e.g. FIFO, CAUSAL, TOTAL) into a single channel (with respect to each of these protocols). Moreover, the proposed abstract channel can handle the mix of any partial or total order protocols. We present a cooperative streaming scenario and an experimental platform for measuring the cost of combining several protocols on various network conditions and show how our coordination service can adjust the degree of synchronization according to network variations. Cezar Plesca, Romulus Grigoras, Philippe Quéinnec, Gérard Padiou, Jean Fanchon |
PDP | 3 |
| 2005 | Streaming with causality: a practical approachabstractHighly interactive collaborative streaming applications express the need for causality. Solutions exist but we argue that more work needs to be done especially from a perceptual point of view. The key question is: given the current state of the Internet and the perceptual tolerance of causal desynchronization, does causality make any difference? This paper proposes a practical answer to this question by comparing different solutions. We support this comparison by producing video results for a live streaming scenario on an experimental platform. Further, this paper proposes a novel approach for handling causality in multimedia and shows that it can perform better than Δ-causality, usually considered the best solution. Cezar Plesca, Romulus Grigoras, Philippe Quéinnec, Gérard Padiou |
ACM Multimedia | 3 |
| 2005 | Cooperative Mobile Agents to Gather Global InformationabstractThis paper describes an original approach to writing reactive algorithms on highly dynamic networks. We propose to use randomly mobile agents to gather global information about such networks. In this model, mobility is twofold: nodes move within the network and agents are able to migrate from node to node by following network links as they exist at a given moment in time. We apply this approach to a toy load balancing example. Through simulations, we illustrate the reactivity and convergence properties of the proposed approach. In particular, we emphasize two points: the solution is well adapted to node mobility in so much as its performance increases with the node mobility rate, and agent cooperation can be used effectively in this context to increase performance Michel Charpentier, Gérard Padiou, Philippe Quéinnec |
NCA | 3 |
| 2000 | Describing Mobile Computations with Path Vectors
Philippe Quéinnec, Mamoun Filali, Philippe Mauran, Gérard Padiou |
OPODIS | 1 |
| 1999 | Modelling and Verifying Migration: A case study
Michel Charpentier, Mamoun Filali, Philippe Mauran, Gérard Padiou, Philippe Quéinnec |
OPODIS | 5 |
| 1994 | Derivation of Fault Tolerance Properties of Distributed AlgorithmsabstractNo abstract available. Philippe Quéinnec, Gérard Padiou |
PODC | 1 |
| 1993 | Flight plan management in a distributed air traffic control systemabstractThe authors explore how large-scale replication can enhance the availability of data in a loosely coupled distributed system. The concern is with air traffic control systems that are geographically distributed and impose strict constraints of availability. In this framework, a replication system providing a weak consistency of data is proposed. The specific properties of flight plan data are studied, and possible replication strategies are discussed. The authors' approach, which is characterized by a split between the propagation function and the end-user service, is then presented.> Philippe Quéinnec, Gérard Padiou |
ISADS | 1 |