Concept

Structure de Kripke

Publications associées (12)

Interplay of Efficient Model Checking and Secure Processor Design: A Case Study on Secure Speculation

There is increasing use of model checking to verify the security of processors, including those with speculative execution. However, model checkers face scalability challenges and are limited in the scale of processors and specific security properties they can currently handle. This research shows how exploiting domain-specific information about the design of secure processors can be used to scale model checking and make it more efficient. Our key observation is that proofs of non-interference properties re

IEEE2026

Uniform Analysis for Communicating Timed Systems (Extended Technical Report)

Languages based on the theory of timed automata are a well established approach for modelling and analysing real-time systems, with many applications both in an industrial and academic context. Model checking for timed automata has been studied extensively during the last two decades; however, even now industrial-grade model checkers are available only for few timed automata dialects (in particular UPPAAL timed automata), exhibit limited scalability for systems with large discrete state space, and cannot ha

2013

Model Checking a Networked System Without the Network

Rachid Guerraoui

Current approaches to model checking distributed systems reduce the problem to that of model checking centralized systems: global states involving all nodes and communication links are systematically explored. The frequent changes in the network element of the global states lead however to a rapid state explosion and make it impossible to model check any non-trivial distributed system. We explore in this paper an alternative: a local approach where the network is ignored, a priori: only the local nodes' sta

2011

Local Model Checking

Rachid Guerraoui

2011

Runtime Instrumentation for Precise Flow-Sensitive Type Analysis

We describe a combination of runtime information and static analysis for checking properties of complex and configurable systems. The basic idea of our approach is to 1) let the program execute and thereby read the important dynamic configuration data, then 2) invoke static analysis from this runtime state to detect possible errors that can happen in the continued execution. This approach improves analysis precision, particularly with respect to types of global variables and nested data structures. It also

2010

DPOR-DS: Dynamic Partial Order Reduction in Distributed Systems

In this paper, we present DPOR-DS, an algorithm for dynamic partial order reduction in model checking of distributed systems. This work is inspired by the techniques introduced in the seminal work of DPOR which is designed for multi-threaded systems. Different characteristics between distributed systems and multi-threaded systems raises new challenges for implementing the idea in distributed system domain. By developing techniques to address those challenges, we prove the soundness and completeness of DPOR-

2009

Antichains For The Automata-Based Approach To Model-Checking

We propose and evaluate antichain algorithms to solve the universality and language inclusion problems for nondeterministic Buchi automata, and the emptiness problem for alternating Buchi automata. To obtain those algorithms, we establish the existence of ...

2009

A Scalable and Oblivious Atomicity Assertion

Rachid Guerraoui

This paper presents SOAR: the first oblivious atomicity assertion with polynomial complexity. SOAR enables to check atomicity of a single-writer multi-reader register implementation. The basic idea underlying the low overhead induced by SOAR lies in greedily checking, in a backward manner, specific points of an execution where register operations could be linearized, rather than exploring all possible precedence relations among these. We illustrate the use of SOAR by implementing it in +CAL. The performance

2008

Using Bounded Model Checking to Verify Consensus Algorithms

André Schiper

This paper presents an approach to automatic verification of asynchronous round-based consensus algorithms. We use model checking, a widely practiced verification method; but its application to asynchronous distributed algorithms is difficult because the state space of these algorithms is often infinite. The proposed approach addresses this difficulty by reducing the verification problem to small model checking problems that involve only single phases of algorithm execution. Because a phase consists of a fi

2008

Discrete choice modelling of combined mode and departure time

Typical daily decision-making process of individuals regarding use of transport system involves mainly three types of decisions: mode choice, departure time choice and route choice. This paper focuses on the mode and departure time choice processes and stu ...

2008

From Liveness to Promptness

Liveness temporal properties state that something

good'' eventually happens, e.g., every request is eventually granted. In Linear Temporal Logic (LTL), there is no a priori bound on the

wait time'' for an eventually to be fulfilled. That is,

F\theta

asserts that

\theta

holds eventually, but there is no bound on the time when

\theta

will hold. This is troubling, as designers tend to interpret an eventuality

\F\theta

as an abstraction of a bounded eventuality

F^{\leq k}\theta

, for an unknown

k

2007

Bounded Asynchrony: A Biologically Inspired Notion of Concurrency

We introduce {\em bounded asynchrony}, a notion of `concurrency tailored to the modeling of biological cell-cell interactions. Bounded asynchrony is the result of a scheduler that bounds the number of steps that one process get ahead of other processes; this allows the components of a system to move independently while keeping them coupled. Bounded asynchrony accurately reproduces the experimental observations made about certain cell-cell interactions: its constrained nondeterminism captures the variability

2007

Graph Chat

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

Publications associées (12)

good'' eventually happens, e.g., every request is eventually granted. In Linear Temporal Logic (LTL), there is no a priori bound on the

wait time'' for an eventually to be fulfilled. That is,

F\theta

asserts that

\theta

holds eventually, but there is no bound on the time when

\theta

will hold. This is troubling, as designers tend to interpret an eventuality

\F\theta

as an abstraction of a bounded eventuality

F^{\leq k}\theta

, for an unknown

k

2007

Bounded Asynchrony: A Biologically Inspired Notion of Concurrency

2007