Publication

Model Checking of Distributed Algorithm Implementations

Related publications (89)

Graph Chatbot

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

Simplifying Distributed System Development

Viktor Kuncak, Dejan Kostic, Maysam Yabandeh, Nedeljko Vasic

Distributed systems are difficult to design and develop. The difficulties arise both in basic safety correctness properties, and in achieving high performance. As a result of this complexity, the implementation of a distributed system often contains the ba ...

2009

Almost-Invariants: From Bugs in Distributed Systems to Invariants

Dejan Kostic, Marco Canini, Maysam Yabandeh, Abhishek Anand

It is notoriously hard to develop dependable distributed systems. This is partly due to the difficulties in foreseeing various corner cases and failure scenarios while implementing a system that will be deployed over an asynchronous network. In contrast, r ...

2009

The Disagreement Power of an Adversary

Rachid Guerraoui

At the heart of distributed computing lies the fundamental result that the level of agreement that can be obtained in an asynchronous shared memory model where t processes can crash is exactly t + 1. In other words, an adversary that can crash any subset o ...

2009

A formal approach to fault tolerant distributed consensus

Rachele Fuzzati

The term distributed Consensus denotes the problem of getting a certain number of processes, that could be far away from each other and that exchange messages through some communication means, to all agree on the same value. This problem has been proved im ...

EPFL2008

Abstractions for asynchronous distributed computing with malicious players

Marko Vukolic

In modern distributed systems, failures are the norm rather than the exception. In many cases, these failures are not benign. Settings such as the Internet might incur malicious (also called Byzantine or arbitrary) behavior and asynchrony. As a result, and ...

EPFL2008

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 s ...

2008

CrystalBall: Predicting and Preventing Inconsistencies in Deployed Distributed Systems

Viktor Kuncak, Dejan Kostic, Maysam Yabandeh, Nikola Knezevic

We propose a new approach for developing and deploying distributed systems, in which nodes predict distributed consequences of their actions, and use this information to detect and avoid errors. Each node continuously runs a state exploration algorithm on ...

2008

Failure detectors as type boosters

Rachid Guerraoui

The power of an object type T can be measured as the maximum number n of processes that can solve consensus using only objects of T and registers. This number, denoted cons(T), is called the consensus power of T. This paper addresses the question of the we ...

Springer-Verlag2008

Efficient Object Placement Including Node Selection in a Distributed Virtual Machine

David Atienza Alonso

Currently, software engineering is becoming even more complex due to distributed computing. In this new context, portability while providing the programmer with the single system image of a classical Java Virtual Machine (JVM) is one of the key issues. Hen ...

IOS Press2008

In Search of Lost Time

Martin Hutle

Dwork, Lynch, and Stockmeyer (1988) and Lamport (1998) showed that, in order to solve Consensus in a distributed system, it is sufficient that the system behaves well during a finite period of time. In sharp contrast, Chandra, Hadzilacos, and Toueg (1996) ...

2008