Josef Widder
YOU?
Author Swipe
View article: A case study on parametric verification of failure detectors
A case study on parametric verification of failure detectors Open
Partial synchrony is a model of computation in many distributed algorithms and modern blockchains. These algorithms are typically parameterized in the number of participants, and their correctness requires the existence of bounds on messag…
View article: Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker
Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker Open
Threshold guards are a basic primitive of many fault-tolerant algorithms that solve classical problems in distributed computing, such as reliable broadcast, two-phase commit, and consensus. Moreover, threshold guards can be found in recent…
View article: Brief Announcement: Holistic Verification of Blockchain Consensus
Brief Announcement: Holistic Verification of Blockchain Consensus Open
International audience
View article: Holistic Verification of Blockchain Consensus
Holistic Verification of Blockchain Consensus Open
Blockchain has recently attracted the attention of the industry due, in part, to its ability to automate asset transfers. It requires distributed participants to reach a consensus on a block despite the presence of malicious (a.k.a. Byzant…
View article: Revisiting Tendermint: Design Tradeoffs, Accountability, and Practical Use
Revisiting Tendermint: Design Tradeoffs, Accountability, and Practical Use Open
Tendermint is a deterministic consensus protocol and is one of the most mature implementations of its kind. This implementation is used as the core for building State Machine Replication (SMR) platforms with Byzantine fault-tolerant (BFT) …
View article: A case study on parametric verification of failure detectors
A case study on parametric verification of failure detectors Open
Partial synchrony is a model of computation in many distributed algorithms and modern blockchains. These algorithms are typically parameterized in the number of participants, and their correctness requires the existence of bounds on messag…
View article: Correction to: Verification of randomized consensus algorithms under round-rigid adversaries
Correction to: Verification of randomized consensus algorithms under round-rigid adversaries Open
A correction to this paper has been published: https://doi.org/10.1007/s10009-021-00612-4
View article: Compositional Verification of Byzantine Consensus
Compositional Verification of Byzantine Consensus Open
Until now, computer-aided proofs of the liveness of byzantine consensus algorithms assumed synchrony to reason in lock steps or the error-prone manual intervention of experts in the proof checker, but could not be automated through model c…
View article: Guard Automata for the Verification of Safety and Liveness of Distributed Algorithms
Guard Automata for the Verification of Safety and Liveness of Distributed Algorithms Open
Distributed algorithms typically run over arbitrary many processes and may involve unboundedly many rounds, making the automated verification of their correctness challenging. Building on domain theory, we introduce a framework that abstra…
View article: Guard Automata for the Verification of Safety and Liveness of Distributed Algorithms (long version)
Guard Automata for the Verification of Safety and Liveness of Distributed Algorithms (long version) Open
Distributed algorithms typically run over arbitrary many processes and may involve unboundedly many rounds, making the automated verification of their correctness challenging. Building on domain theory, we introduce a framework that abstra…
View article: Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker
Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker Open
Threshold guards are a basic primitive of many fault-tolerant algorithms that solve classical problems in distributed computing, such as reliable broadcast, two-phase commit, and consensus. Moreover, threshold guards can be found in recent…
View article: Programming at the edge of synchrony
Programming at the edge of synchrony Open
Synchronization primitives for fault-tolerant distributed systems that ensure an effective and efficient cooperation among processes are an important challenge in the programming languages community. We present a new programming abstractio…
View article: A Tendermint Light Client
A Tendermint Light Client Open
In Tendermint blockchains, the proof-of-stake mechanism and the underlying consensus algorithm entail a dynamic fault model that implies that the active validators (nodes that sign blocks) may change over time, and a quorum of these valida…
View article: What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms
What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms Open
The final publication is available via https://doi.org/10.1007/978-3-319-41579-6_2.
View article: Formal Specification and Model Checking of the Tendermint Blockchain Synchronization Protocol (Short Paper)
Formal Specification and Model Checking of the Tendermint Blockchain Synchronization Protocol (Short Paper) Open
Blockchain synchronization is one of the core protocols of Tendermint blockchains. In this short paper, we discuss our recent efforts in formal specification of the protocol and its implementation, as well as some initial model checking re…
View article: Executable Rounds: a Programming Abstraction for Fault-Tolerant Protocols
Executable Rounds: a Programming Abstraction for Fault-Tolerant Protocols Open
Fault-tolerant distributed systems are notoriously difficult to design and implement. Although programming languages for distributed systems is an active research area, appropriate synchronization primitives for fault-tolerance and group c…
View article: Verification of Randomized Distributed Algorithms under Round-Rigid Adversaries
Verification of Randomized Distributed Algorithms under Round-Rigid Adversaries Open
Experiments presented in this paper were carried out using the Grid5000 testbed, supported by a scientific interest group hosted by Inria and including CNRS, RENATER and several Universities as well as other organizations, see grid5000.fr
View article: Communication-closed asynchronous protocols
Communication-closed asynchronous protocols Open
Fault-tolerant distributed systems are implemented over asyn-chronous networks, so that they use algorithms for asynchronous models with faults. Due to asynchronous communication and the occurrence of faults (e.g., process crashes or the n…
View article: Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking
Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking Open
International audience
View article: Communication-Closed Asynchronous Protocols
Communication-Closed Asynchronous Protocols Open
The verification of asynchronous fault-tolerant distributed systems is challenging due to unboundedly many interleavings and network failures (e.g., processes crash or message loss). We propose a method that reduces the verification of asy…
View article: Verification of Randomized Consensus Algorithms Under Round-Rigid Adversaries
Verification of Randomized Consensus Algorithms Under Round-Rigid Adversaries Open
Randomized fault-tolerant distributed algorithms pose a number of challenges for automated verification: (i) parameterization in the number of processes and faults, (ii) randomized choices and probabilistic properties, and (iii) an unbound…
View article: Reducing asynchrony to synchronized rounds
Reducing asynchrony to synchronized rounds Open
Synchronous computation models simplify the design and the verification of fault-tolerant distributed systems. For efficiency reasons such systems are designed and implemented using an asynchronous semantics. In this paper, we bridge the g…