| 2022 | DSN | Revisiting Tendermint: Design Tradeoffs, Accountability, and Practical Use. | Ethan Buchman, Rachid Guerraoui, Jovan Komatovic, Zarko Milosevic, Dragos-Adrian Seredinschi, Josef Widder |
| 2022 | PODC | Brief Announcement: Holistic Verification of Blockchain Consensus. | Nathalie Bertrand, Vincent Gramoli, Igor Konnov, Marijana Lazic, Pierre Tholoniat, Josef Widder |
| 2021 | CONCUR | Guard Automata for the Verification of Safety and Liveness of Distributed Algorithms. | Nathalie Bertrand, Bastien Thomas, Josef Widder |
| 2021 | FORTE | A Case Study on Parametric Verification of Failure Detectors. | Thanh-Hai Tran, Igor Konnov, Josef Widder |
| 2021 | VMCAI | A Reduction Theorem for Randomized Distributed Algorithms Under Weak Adversaries. | Nathalie Bertrand, Marijana Lazic, Josef Widder |
| 2021 | VMCAI | Eliminating Message Counters in Synchronous Threshold Automata. | Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger |
| 2020 | ATVA | Eliminating Message Counters in Threshold Automata. | Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger |
| 2020 | CAV | Formal Specification and Model Checking of the Tendermint Blockchain Synchronization Protocol (Short Paper). | Sean Braithwaite, Ethan Buchman, Igor Konnov, Zarko Milosevic, Ilina Stoilkovska, Josef Widder, Anca Zamfir |
| 2020 | FORTE | Tutorial: Parameterized Verification with Byzantine Model Checker. | Igor Konnov, Marijana Lazic, Ilina Stoilkovska, Josef Widder |
| 2020 | ISoLA | Tendermint Blockchain Synchronization: Formal Specification and Model Checking. | Sean Braithwaite, Ethan Buchman, Igor Konnov, Zarko Milosevic, Ilina Stoilkovska, Josef Widder, Anca Zamfir |
| 2019 | CAV | Communication-Closed Asynchronous Protocols. | Andrei Damian, Cezara Dragoi, Alexandru Militaru, Josef Widder |
| 2019 | CONCUR | Verification of Randomized Consensus Algorithms Under Round-Rigid Adversaries. | Nathalie Bertrand, Igor Konnov, Marijana Lazic, Josef Widder |
| 2019 | TACAS | Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking. | Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger |
| 2018 | CONCUR | Reachability in Parameterized Systems: All Flavors of Threshold Automata. | Jure Kukovec, Igor Konnov, Josef Widder |
| 2018 | ISoLA | ByMC: Byzantine Model Checker. | Igor Konnov, Josef Widder |
| 2018 | VMCAI | Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction. | Benjamin Aminof, Sasha Rubin, Ilina Stoilkovska, Josef Widder, Florian Zuleger |
| 2017 | OPODIS | Synthesis of Distributed Algorithms with Parameterized Threshold Guards. | Marijana Lazic, Igor Konnov, Josef Widder, Roderick Bloem |
| 2017 | POPL | A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms. | Igor V. Konnov, Marijana Lazic, Helmut Veith, Josef Widder |
| 2017 | VMCAI | Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms. | Igor V. Konnov, Josef Widder, Francesco Spegni, Luca Spalazzi |
| 2015 | CAV | SMT and POR Beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms. | Igor Konnov, Helmut Veith, Josef Widder |
| 2014 | CONCUR | On the Completeness of Bounded Model Checking for Threshold-Based Distributed Algorithms: Reachability. | Igor Konnov, Helmut Veith, Josef Widder |
| 2014 | NCA | Solvability-Based Comparison of Failure Detectors. | Srikanth Sastry, Josef Widder |
| 2014 | VMCAI | A Logic-Based Framework for Verifying Consensus Algorithms. | Cezara Dragoi, Thomas A. Henzinger, Helmut Veith, Josef Widder, Damien Zufferey |
| 2013 | FMCAD | Parameterized model checking of fault-tolerant distributed algorithms by abstraction. | Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder |
| 2013 | PODC | Brief announcement: parameterized model checking of fault-tolerant distributed algorithms by abstraction. | Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder |
| 2012 | CONCUR | Efficient Checking of Link-Reversal-Based Concurrent Systems. | Matthias Fgger, Josef Widder |
| 2012 | OPODIS | Wait-Free Stabilizing Dining Using Regular Registers. | Srikanth Sastry, Jennifer L. Welch, Josef Widder |
| 2011 | SPAA | Brief announcement: full reversal routing as a linear dynamical system. | Bernadette Charron-Bost, Matthias Fgger, Jennifer L. Welch, Josef Widder |
| 2011 | SIROCCO | Full Reversal Routing as a Linear Dynamical System. | Bernadette Charron-Bost, Matthias Fgger, Jennifer L. Welch, Josef Widder |
| 2011 | SIROCCO | Partial is Full. | Bernadette Charron-Bost, Matthias Fgger, Jennifer L. Welch, Josef Widder |
| 2009 | Algosensors | Link Reversal: How to Play Better to Work Less. | Bernadette Charron-Bost, Jennifer L. Welch, Josef Widder |
| 2009 | SPAA | Routing without ordering. | Bernadette Charron-Bost, Antoine Gaillard, Jennifer L. Welch, Josef Widder |
| 2007 | DSN | Synchronous Consensus with Mortal Byzantines. | Josef Widder, Gnther Gridling, Bettina Weiss, Jean-Paul Blanquart |
| 2007 | OPODIS | Clock Synchronization in the Byzantine-Recovery Failure Model. | Emmanuelle Anceaume, Carole Delporte-Gallet, Hugues Fauconnier, Michel Hurfin, Josef Widder |
| 2007 | PODC | Tolerating corrupted communication. | Martin Biely, Josef Widder, Bernadette Charron-Bost, Antoine Gaillard, Martin Hutle, Andr Schiper |
| 2007 | SSS | Relating Stabilizing Timing Assumptions to Stabilizing Failure Detectors Regarding Solvability and Efficiency. | Martin Biely, Martin Hutle, Lucia Draque Penso, Josef Widder |
| 2006 | SSS | Optimal Message-Driven Implementation of Omega with Mute Processes. | Martin Biely, Josef Widder |
| 2005 | EDCC | Failure Detection with Booting in Partially Synchronous Systems. | Josef Widder, Grard Le Lann, Ulrich Schmid |
| 2005 | OPODIS | Implementing Reliable Distributed Real-Time Systems with the | Jean-Franois Hermant, Josef Widder |
| 2005 | PODC | Brief announcement: on the possibility and the impossibility of message-driven self-stabilizing failure detection. | Martin Hutle, Josef Widder |
| 2005 | SSS | On the Possibility and the Impossibility of Message-Driven Self-stabilizing Failure Detection. | Martin Hutle, Josef Widder |