Josef Widder

Dragos-Adrian Seredinschi

Log. Methods Comput. Sci., 2023

Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2023

2022

Verifying safety of synchronous fault-tolerant algorithms by bounded model checking.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2022

Holistic Verification of Blockchain Consensus.

[BibT_eX]

[DOI]

Proceedings of the 36th International Symposium on Distributed Computing, 2022

Brief Announcement: Holistic Verification of Blockchain Consensus.

[BibT_eX]

[DOI]

Proceedings of the PODC '22: ACM Symposium on Principles of Distributed Computing, Salerno, Italy, July 25, 2022

Revisiting Tendermint: Design Tradeoffs, Accountability, and Practical Use.

[BibT_eX]

[DOI]

Proceedings of the 52nd Annual IEEE/IFIP International Conference on Dependable Systems and Networks, 2022

2021

Correction to: Verification of randomized consensus algorithms under round-rigid adversaries.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2021

Verification of randomized consensus algorithms under round-rigid adversaries.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2021

Eliminating Message Counters in Synchronous Threshold Automata.

[BibT_eX]

[DOI]

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2021

A Reduction Theorem for Randomized Distributed Algorithms Under Weak Adversaries.

[BibT_eX]

[DOI]

Nathalie Bertrand

Marijana Lazic

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2021

Guard Automata for the Verification of Safety and Liveness of Distributed Algorithms.

[BibT_eX]

[DOI]

Nathalie Bertrand

Bastien Thomas

Proceedings of the 32nd International Conference on Concurrency Theory, 2021

2020

Programming at the edge of synchrony.

[BibT_eX]

[DOI]

Cezara Dragoi

Damien Zufferey

Proc. ACM Program. Lang., 2020

A Tendermint Light Client.

[BibT_eX]

[DOI]

CoRR, 2020

Cutoffs for Symmetric Point-to-Point Distributed Algorithms.

[BibT_eX]

[DOI]

Thanh-Hai Tran

Proceedings of the Networked Systems - 8th International Conference, 2020

Tendermint Blockchain Synchronization: Formal Specification and Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles, 2020

Tutorial: Parameterized Verification with Byzantine Model Checker.

[BibT_eX]

[DOI]

Proceedings of the Formal Techniques for Distributed Objects, Components, and Systems, 2020

Formal Specification and Model Checking of the Tendermint Blockchain Synchronization Protocol (Short Paper).

[BibT_eX]

[DOI]

Proceedings of the 2nd Workshop on Formal Methods for Blockchains, 2020

Eliminating Message Counters in Threshold Automata.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2020

2019

Communication-Closed Asynchronous Protocols.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

2018

Reducing asynchrony to synchronized rounds.

[BibT_eX]

[DOI]

Cezara Dragoi

CoRR, 2018

Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction.

[BibT_eX]

[DOI]

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2018

ByMC: Byzantine Model Checker.

[BibT_eX]

[DOI]

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems, 2018

Reachability in Parameterized Systems: All Flavors of Threshold Automata.

[BibT_eX]

[DOI]

Jure Kukovec

Proceedings of the 29th International Conference on Concurrency Theory, 2018

2017

On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability.

[BibT_eX]

[DOI]

Igor V. Konnov

Helmut Veith

Inf. Comput., 2017

Para<sup>2</sup>: parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2017

Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms.

[BibT_eX]

[DOI]

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2017

A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms.

[BibT_eX]

[DOI]

Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

Synthesis of Distributed Algorithms with Parameterized Threshold Guards.

[BibT_eX]

[DOI]

Proceedings of the 21st International Conference on Principles of Distributed Systems, 2017

2016

Decidability in Parameterized Verification.

[BibT_eX]

[DOI]

SIGACT News, 2016

2015

Decidability of Parameterized Verification

[BibT_eX]

[DOI]

Synthesis Lectures on Distributed Computing Theory, Morgan & Claypool Publishers, ISBN: 978-3-031-02011-7, 2015

Time Complexity of Link Reversal Routing.

[BibT_eX]

[DOI]

ACM Trans. Algorithms, 2015

What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms.

[BibT_eX]

[DOI]

Igor V. Konnov

Helmut Veith

Proceedings of the Perspectives of System Informatics, 2015

SMT and POR Beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms.

[BibT_eX]

[DOI]

Helmut Veith

Proceedings of the Computer Aided Verification - 27th International Conference, 2015

2014

A Logic-Based Framework for Verifying Consensus Algorithms.

[BibT_eX]

[DOI]

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2014

Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Executable Software Models, 2014

Solvability-Based Comparison of Failure Detectors.

[BibT_eX]

[DOI]

Srikanth Sastry

Proceedings of the 2014 IEEE 13th International Symposium on Network Computing and Applications, 2014

2013

Link Reversal Routing with Binary Link Labels: Work Complexity.

[BibT_eX]

[DOI]

Antoine Gaillard

SIAM J. Comput., 2013

Formal Verification of Distributed Algorithms (Dagstuhl Seminar 13141).

[BibT_eX]

[DOI]

Stephan Merz

Andrey Rybalchenko

Dagstuhl Reports, 2013

Towards Modeling and Model Checking Fault-Tolerant Distributed Algorithms.

[BibT_eX]

[DOI]

Proceedings of the Model Checking Software - 20th International Symposium, 2013

Brief announcement: parameterized model checking of fault-tolerant distributed algorithms by abstraction.

[BibT_eX]

[DOI]

Proceedings of the ACM Symposium on Principles of Distributed Computing, 2013

Parameterized model checking of fault-tolerant distributed algorithms by abstraction.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 2013

2012

Consensus in the presence of mortal Byzantine faulty processes.

[BibT_eX]

[DOI]

Distributed Comput., 2012

Counter Attack on Byzantine Generals: Parameterized Model Checking of Fault-tolerant Distributed Algorithms

[BibT_eX]

[DOI]

CoRR, 2012

Starting a Dialog between Model Checking and Fault-tolerant Distributed Algorithms

[BibT_eX]

[DOI]

CoRR, 2012

Wait-Free Stabilizing Dining Using Regular Registers.

[BibT_eX]

[DOI]

Srikanth Sastry

Proceedings of the Principles of Distributed Systems, 16th International Conference, 2012

Efficient Checking of Link-Reversal-Based Concurrent Systems.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2012 - Concurrency Theory - 23rd International Conference, 2012

2011

Brief announcement: full reversal routing as a linear dynamical system.

[BibT_eX]

[DOI]

Proceedings of the SPAA 2011: Proceedings of the 23rd Annual ACM Symposium on Parallelism in Algorithms and Architectures, 2011

Partial is Full.

[BibT_eX]

[DOI]

Proceedings of the Structural Information and Communication Complexity, 2011

Full Reversal Routing as a Linear Dynamical System.

[BibT_eX]

[DOI]

Proceedings of the Structural Information and Communication Complexity, 2011

2010

In search of lost time.

[BibT_eX]

[DOI]

Inf. Process. Lett., 2010

2009

Optimal message-driven implementations of omega with mute processes.

[BibT_eX]

[DOI]

Martin Biely

ACM Trans. Auton. Adapt. Syst., 2009

The Theta-Model: achieving synchrony without clocks.

[BibT_eX]

[DOI]

Ulrich Schmid

Distributed Comput., 2009

Routing without ordering.

[BibT_eX]

[DOI]

Antoine Gaillard

Proceedings of the SPAA 2009: Proceedings of the 21st Annual ACM Symposium on Parallelism in Algorithms and Architectures, 2009

Link Reversal: How to Play Better to Work Less.

[BibT_eX]

[DOI]

Proceedings of the Algorithmic Aspects of Wireless Sensor Networks, 2009

2007

Booting clock synchronization in partially synchronous systems with hybrid process and link failures.

[BibT_eX]

[DOI]

Ulrich Schmid

Distributed Comput., 2007

Relating Stabilizing Timing Assumptions to Stabilizing Failure Detectors Regarding Solvability and Efficiency.

[BibT_eX]

[DOI]

Proceedings of the Stabilization, 2007

Tolerating corrupted communication.

[BibT_eX]

[DOI]

Martin Biely

Antoine Gaillard

André Schiper

Proceedings of the Twenty-Sixth Annual ACM Symposium on Principles of Distributed Computing, 2007

Clock Synchronization in the Byzantine-Recovery Failure Model.

[BibT_eX]

[DOI]

Emmanuelle Anceaume

Carole Delporte-Gallet

Hugues Fauconnier

Michel Hurfin

Proceedings of the Principles of Distributed Systems, 11th International Conference, 2007

Synchronous Consensus with Mortal Byzantines.

[BibT_eX]

[DOI]

Proceedings of the 37th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, 2007

2006

Optimal Message-Driven Implementation of Omega with Mute Processes.

[BibT_eX]

[DOI]

Martin Biely

Proceedings of the Stabilization, 2006

2005

On the Possibility and the Impossibility of Message-Driven Self-stabilizing Failure Detection.

[BibT_eX]

[DOI]

Proceedings of the Self-Stabilizing Systems, 2005

Brief announcement: on the possibility and the impossibility of message-driven self-stabilizing failure detection.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Fourth Annual ACM Symposium on Principles of Distributed Computing, 2005

Self-Stabilizing Failure Detector Algorithms.

[BibT_eX]

Proceedings of the IASTED International Conference on Parallel and Distributed Computing and Networks, 2005

Implementing Reliable Distributed Real-Time Systems with the <i>Theta</i>-Model.

[BibT_eX]

[DOI]

Jean-François Hermant

Proceedings of the Principles of Distributed Systems, 9th International Conference, 2005

Failure Detection with Booting in Partially Synchronous Systems.

[BibT_eX]

[DOI]

Gérard Le Lann

Ulrich Schmid

Proceedings of the Dependable Computing, 2005

2003

Booting clock Synchronization in Partially Synchronous Systems.

[BibT_eX]

[DOI]

Proceedings of the Distributed Computing, 17th International Conference, 2003

1992

Adaptive cluster growth: a new algorithm for circuit placement in rectilinear regions.

[BibT_eX]

[DOI]

Chong-Min Kyung

Dieter A. Mlynski

Comput. Aided Des., 1992

1990

Adaptive Cluster Growth (ACG): a new algorithm for circuit packing in rectilinear region.

[BibT_eX]

[DOI]

Chong-Min Kyung