Adaptive Cluster Growth (ACG): a new algorithm for circuit packing in rectilinear region. - Chong-Min Kyung; Josef Widder; Dieter A. Mlynski (EURO-DAC, 1990)

Adaptive cluster growth: a new algorithm for circuit placement in rectilinear regions. - Chong-Min Kyung; Josef Widder; Dieter A. Mlynski (Comput. Aided Des., 1992)

Booting clock Synchronization in Partially Synchronous Systems. - Josef Widder (DISC, 2003)

Failure Detection with Booting in Partially Synchronous Systems. - Josef Widder; Gérard Le Lann; Ulrich Schmid 001 (EDCC, 2005)

Implementing Reliable Distributed Real-Time Systems with the Theta-Model. - Jean-François Hermant; Josef Widder (OPODIS, 2005)

Self-Stabilizing Failure Detector Algorithms. - Martin Hutle; Josef Widder (Parallel and Distributed Computing and Networks, 2005)

Brief announcement: on the possibility and the impossibility of message-driven self-stabilizing failure detection. - Martin Hutle; Josef Widder (PODC, 2005)

On the Possibility and the Impossibility of Message-Driven Self-stabilizing Failure Detection. - Martin Hutle; Josef Widder (Self-Stabilizing Systems, 2005)

Optimal Message-Driven Implementation of Omega with Mute Processes. - Martin Biely; Josef Widder (SSS, 2006)

Synchronous Consensus with Mortal Byzantines. - Josef Widder; Günther Gridling; Bettina Weiss; Jean-Paul Blanquart (DSN, 2007)

Clock Synchronization in the Byzantine-Recovery Failure Model. - Emmanuelle Anceaume; Carole Delporte-Gallet; Hugues Fauconnier; Michel Hurfin; Josef Widder (OPODIS, 2007)

Tolerating corrupted communication. - Martin Biely; Josef Widder; Bernadette Charron-Bost; Antoine Gaillard; Martin Hutle; André Schiper (PODC, 2007)

Relating Stabilizing Timing Assumptions to Stabilizing Failure Detectors Regarding Solvability and Efficiency. - Martin Biely; Martin Hutle; Lucia Draque Penso; Josef Widder (SSS, 2007)

Booting clock synchronization in partially synchronous systems with hybrid process and link failures. - Josef Widder; Ulrich Schmid 001 (Distributed Comput., 2007)

Link Reversal: How to Play Better to Work Less. - Bernadette Charron-Bost; Jennifer L. Welch; Josef Widder (ALGOSENSORS, 2009)

Routing without ordering. - Bernadette Charron-Bost; Antoine Gaillard; Jennifer L. Welch; Josef Widder (SPAA, 2009)

The Theta-Model: achieving synchrony without clocks. - Josef Widder; Ulrich Schmid 001 (Distributed Comput., 2009)

Optimal message-driven implementations of omega with mute processes. - Martin Biely; Josef Widder (ACM Trans. Auton. Adapt. Syst., 2009)

In search of lost time. - Bernadette Charron-Bost; Martin Hutle; Josef Widder (Inf. Process. Lett., 2010)

Full Reversal Routing as a Linear Dynamical System. - Bernadette Charron-Bost; Matthias Függer; Jennifer L. Welch; Josef Widder (SIROCCO, 2011)

Partial is Full. - Bernadette Charron-Bost; Matthias Függer; Jennifer L. Welch; Josef Widder (SIROCCO, 2011)

Brief announcement: full reversal routing as a linear dynamical system. - Bernadette Charron-Bost; Matthias Függer; Jennifer L. Welch; Josef Widder (SPAA, 2011)

Efficient Checking of Link-Reversal-Based Concurrent Systems. - Matthias Függer; Josef Widder (CONCUR, 2012)

Wait-Free Stabilizing Dining Using Regular Registers. - Srikanth Sastry; Jennifer L. Welch; Josef Widder (OPODIS, 2012)

Starting a Dialog between Model Checking and Fault-tolerant Distributed Algorithms - Annu John; Igor Konnov 001; Ulrich Schmid 001; Helmut Veith; Josef Widder (CoRR, 2012)

Counter Attack on Byzantine Generals: Parameterized Model Checking of Fault-tolerant Distributed Algorithms - Annu John; Igor Konnov 001; Ulrich Schmid 001; Helmut Veith; Josef Widder (CoRR, 2012)

Consensus in the presence of mortal Byzantine faulty processes. - Josef Widder; Martin Biely; Günther Gridling; Bettina Weiss; Jean-Paul Blanquart (Distributed Comput., 2012)

Parameterized model checking of fault-tolerant distributed algorithms by abstraction. - Annu John; Igor Konnov 001; Ulrich Schmid 001; Helmut Veith; Josef Widder (FMCAD, 2013)

Brief announcement: parameterized model checking of fault-tolerant distributed algorithms by abstraction. - Annu John; Igor Konnov 001; Ulrich Schmid 001; Helmut Veith; Josef Widder (PODC, 2013)

Towards Modeling and Model Checking Fault-Tolerant Distributed Algorithms. - Annu John; Igor Konnov 001; Ulrich Schmid 001; Helmut Veith; Josef Widder (SPIN, 2013)

Formal Verification of Distributed Algorithms (Dagstuhl Seminar 13141). - Bernadette Charron-Bost; Stephan Merz; Andrey Rybalchenko; Josef Widder (Dagstuhl Reports, 2013)

Link Reversal Routing with Binary Link Labels: Work Complexity. - Bernadette Charron-Bost; Antoine Gaillard; Jennifer L. Welch; Josef Widder (SIAM J. Comput., 2013)

Solvability-Based Comparison of Failure Detectors. - Srikanth Sastry; Josef Widder (NCA, 2014)

Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms. - Annu Gmeiner; Igor Konnov 001; Ulrich Schmid 001; Helmut Veith; Josef Widder (SFM, 2014)

A Logic-Based Framework for Verifying Consensus Algorithms. - Cezara Dragoi; Thomas A. Henzinger; Helmut Veith; Josef Widder; Damien Zufferey (VMCAI, 2014)

SMT and POR Beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms. - Igor Konnov 001; Helmut Veith; Josef Widder (CAV (1), 2015)

What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms. - Igor V. Konnov 001; Helmut Veith; Josef Widder (Ershov Memorial Conference, 2015)

Time Complexity of Link Reversal Routing. - Bernadette Charron-Bost; Matthias Függer; Jennifer L. Welch; Josef Widder (ACM Trans. Algorithms, 2015)

Decidability of Parameterized Verification - Roderick Bloem; Swen Jacobs; Ayrat Khalimov 001; Igor Konnov 001; Sasha Rubin; Helmut Veith; Josef Widder (Morgan & Claypool Publishers, 2015)

Decidability in Parameterized Verification. - Roderick Bloem; Swen Jacobs; Ayrat Khalimov 001; Igor Konnov 001; Sasha Rubin; Helmut Veith; Josef Widder (SIGACT News, 2016)

Synthesis of Distributed Algorithms with Parameterized Threshold Guards. - Marijana Lazic; Igor Konnov 001; Josef Widder; Roderick Bloem (OPODIS, 2017)

A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms. - Igor V. Konnov 001; Marijana Lazic; Helmut Veith; Josef Widder (POPL, 2017)

Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms. - Igor V. Konnov 001; Josef Widder; Francesco Spegni; Luca Spalazzi (VMCAI, 2017)

Para2: parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms. - Igor Konnov 001; Marijana Lazic; Helmut Veith; Josef Widder (Formal Methods Syst. Des., 2017)

On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability. - Igor V. Konnov 001; Helmut Veith; Josef Widder (Inf. Comput., 2017)

Reachability in Parameterized Systems: All Flavors of Threshold Automata. - Jure Kukovec; Igor Konnov 001; Josef Widder (CONCUR, 2018)

ByMC: Byzantine Model Checker. - Igor Konnov 001; Josef Widder (ISoLA (3), 2018)

Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction. - Benjamin Aminof; Sasha Rubin; Ilina Stoilkovska; Josef Widder; Florian Zuleger (VMCAI, 2018)

Reducing asynchrony to synchronized rounds. - Cezara Dragoi; Josef Widder (CoRR, 2018)

Communication-Closed Asynchronous Protocols. - Andrei Damian; Cezara Dragoi; Alexandru Militaru; Josef Widder (CAV (2), 2019)

Eliminating Message Counters in Threshold Automata. - Ilina Stoilkovska; Igor Konnov 001; Josef Widder; Florian Zuleger (ATVA, 2020)

Formal Specification and Model Checking of the Tendermint Blockchain Synchronization Protocol (Short Paper). - Sean Braithwaite; Ethan Buchman; Igor Konnov 001; Zarko Milosevic 001; Ilina Stoilkovska; Josef Widder; Anca Zamfir (FMBC@CAV, 2020)

Tutorial: Parameterized Verification with Byzantine Model Checker. - Igor Konnov 001; Marijana Lazic; Ilina Stoilkovska; Josef Widder (FORTE, 2020)

Tendermint Blockchain Synchronization: Formal Specification and Model Checking. - Sean Braithwaite; Ethan Buchman; Igor Konnov 001; Zarko Milosevic 001; Ilina Stoilkovska; Josef Widder; Anca Zamfir (ISoLA (1), 2020)

Cutoffs for Symmetric Point-to-Point Distributed Algorithms. - Thanh-Hai Tran 002; Igor Konnov 001; Josef Widder (NETYS, 2020)

A Tendermint Light Client. - Sean Braithwaite; Ethan Buchman; Ismail Khoffi; Igor Konnov 001; Zarko Milosevic 001; Romain Ruetschi; Josef Widder (CoRR, 2020)

Programming at the edge of synchrony. - Cezara Dragoi; Josef Widder; Damien Zufferey (Proc. ACM Program. Lang., 2020)

Guard Automata for the Verification of Safety and Liveness of Distributed Algorithms. - Nathalie Bertrand 001; Bastien Thomas; Josef Widder (CONCUR, 2021)

A Reduction Theorem for Randomized Distributed Algorithms Under Weak Adversaries. - Nathalie Bertrand 001; Marijana Lazic; Josef Widder (VMCAI, 2021)

Eliminating Message Counters in Synchronous Threshold Automata. - Ilina Stoilkovska; Igor Konnov 001; Josef Widder; Florian Zuleger (VMCAI, 2021)

Verification of randomized consensus algorithms under round-rigid adversaries. - Nathalie Bertrand 001; Igor Konnov 001; Marijana Lazic; Josef Widder (Int. J. Softw. Tools Technol. Transf., 2021)

Correction to: Verification of randomized consensus algorithms under round-rigid adversaries. - Nathalie Bertrand 001; Igor Konnov 001; Marijana Lazic; Josef Widder (Int. J. Softw. Tools Technol. Transf., 2021)

Revisiting Tendermint: Design Tradeoffs, Accountability, and Practical Use. - Ethan Buchman; Rachid Guerraoui; Jovan Komatovic; Zarko Milosevic 001; Dragos-Adrian Seredinschi; Josef Widder (DSN (Supplements), 2022)

Brief Announcement: Holistic Verification of Blockchain Consensus. - Nathalie Bertrand 001; Vincent Gramoli; Igor Konnov 001; Marijana Lazic; Pierre Tholoniat; Josef Widder (PODC, 2022)

Holistic Verification of Blockchain Consensus. - Nathalie Bertrand 001; Vincent Gramoli; Igor Konnov 001; Marijana Lazic; Pierre Tholoniat; Josef Widder (DISC, 2022)

Verifying safety of synchronous fault-tolerant algorithms by bounded model checking. - Ilina Stoilkovska; Igor Konnov 001; Josef Widder; Florian Zuleger (Int. J. Softw. Tools Technol. Transf., 2022)

Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker. - Igor Konnov 001; Marijana Lazic; Ilina Stoilkovska; Josef Widder (Log. Methods Comput. Sci., 2023)

A case study on parametric verification of failure detectors. - Thanh-Hai Tran 002; Igor Konnov 001; Josef Widder (Log. Methods Comput. Sci., 2023)