Publication

Efficient Model Checking of Fault-Tolerant Distributed Protocols

Related publications (32)

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.

How to Specify and How to Prove Correctness of Secure Routing Protocols for MANET

Jean-Pierre Hubaux, Panagiotis Papadimitratos

Secure routing protocols for mobile ad hoc networks have been developed recently, yet, it has been unclear what are the properties they achieve, as a formal analysis of these protocols is mostly lacking. In this paper, we are concerned with this problem, h ...

2006

EPICURE : A Partitioning and CoDesign Framework For Reconfigurable Computing

Sébastien Bilavarn

This paper presents a new global design methodology capable to bridge the gap between an abstract specification level and a heterogeneous reconfigurable architecture level. The Epicure contribution is the result of a joint study on abstraction/refinement m ...

2006

Comparing the Performance of Two Consensus Algorithms with Centralized and Decentralized Communication Schemes

André Schiper

Comparing the Performance of Two Consensus Algorithms with Centralized and Decentralized Communication Schemes Peter Urban and Andre Schiper Protocols that solve agreement problems are essential building blocks for fault tolerant distributed systems. While ...

2004

Debugging Temporal Specifications with Concept Analysis

James Richard Larus

Program verification tools (such as model checkers and static analyzers) can find many errors in programs. These tools need formal specifications of correct program behavior, but writing a correct specification is difficult, just as writing a correct progr ...

ACM2003

Mining Specifications

James Richard Larus

Program verification is a promising approach to improving program quality, because it can search all possible program executions for specific errors. However, the need to formally describe correct behavior or errors is a major barrier to the widespread ado ...

ACM2002

Building blocks for secure services

Levente Buttyan

This thesis is concerned with two security mechanisms: authenticated key transport and rational exchange protocols. These mechanisms are potential building blocks in the security architecture of a range of different services. Authenticated key transport pr ...

EPFL2002

The TL Compiler

This paper describes a method of compiling specification properties into automata or test oracles which allow testing of any proposed implementation. It also shows how to interpret the automata's status during testing. The method addresses verification of ...

2000

Developing safe concurrent and distributed applications with an architectural environment

The developing environment presented in the paper is built around an interactive tool that can accompany the software engineer for the whole software development process of concurrent and distributed applications. This environment relies on a concept of ac ...

IEEE Comput. Soc1999

A system engineering methodology integrating performance evaluation and formal specification

The situation of telecommunications systems is rapidly evolving towards a state characterized by the presence of a multitude of services integrated in a single network structure. In order to ease their integration, it is important to provide an unambiguous ...

EPFL1996

Teapot: Language Support for Writing Memory Coherence Protocols

James Richard Larus

Recent shared-memory parallel computer systems offer the exciting possibility of customizing memory coherence protocols to fit an application's semantics and sharing patterns. Custom protocols have been used to achieve message-passing performance---while r ...

ACM1996