Josef Widder

Publication Activity (10 Years)

Years Active: 1990-2023
Publications (10 Years): 39

Top Topics

Epistemic Logic

Formal Specification

Orders Of Magnitude

Interconnection Networks

Top Venues

Int. J. Softw. Tools Technol. Transf.

Publications

Thanh-Hai Tran, Igor Konnov, Josef Widder
A case study on parametric verification of failure detectors. Log. Methods Comput. Sci. 19 (1) (2023)
Igor Konnov, Marijana Lazic, Ilina Stoilkovska, Josef Widder
Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker. Log. Methods Comput. Sci. 19 (1) (2023)
Nathalie Bertrand, Vincent Gramoli, Igor Konnov, Marijana Lazic, Pierre Tholoniat, Josef Widder
Brief Announcement: Holistic Verification of Blockchain Consensus. PODC (2022)
Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger
Verifying safety of synchronous fault-tolerant algorithms by bounded model checking. Int. J. Softw. Tools Technol. Transf. 24 (1) (2022)
Ethan Buchman, Rachid Guerraoui, Jovan Komatovic, Zarko Milosevic, Dragos-Adrian Seredinschi, Josef Widder
Revisiting Tendermint: Design Tradeoffs, Accountability, and Practical Use. DSN (Supplements) (2022)
Nathalie Bertrand, Vincent Gramoli, Igor Konnov, Marijana Lazic, Pierre Tholoniat, Josef Widder
Holistic Verification of Blockchain Consensus. CoRR (2022)
Nathalie Bertrand, Vincent Gramoli, Igor Konnov, Marijana Lazic, Pierre Tholoniat, Josef Widder
Holistic Verification of Blockchain Consensus. DISC (2022)
Nathalie Bertrand, Igor Konnov, Marijana Lazic, Josef Widder
Correction to: Verification of randomized consensus algorithms under round-rigid adversaries. Int. J. Softw. Tools Technol. Transf. 23 (5) (2021)
Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger
Eliminating Message Counters in Synchronous Threshold Automata. VMCAI (2021)
Nathalie Bertrand, Bastien Thomas, Josef Widder
Guard Automata for the Verification of Safety and Liveness of Distributed Algorithms. CONCUR (2021)
Nathalie Bertrand, Igor Konnov, Marijana Lazic, Josef Widder
Verification of randomized consensus algorithms under round-rigid adversaries. Int. J. Softw. Tools Technol. Transf. 23 (5) (2021)
Thanh-Hai Tran, Igor Konnov, Josef Widder
A case study on parametric verification of failure detectors. CoRR (2021)
Nathalie Bertrand, Marijana Lazic, Josef Widder
A Reduction Theorem for Randomized Distributed Algorithms Under Weak Adversaries. VMCAI (2021)
Thanh-Hai Tran, Igor Konnov, Josef Widder
A Case Study on Parametric Verification of Failure Detectors. FORTE (2021)
Sean Braithwaite, Ethan Buchman, Ismail Khoffi, Igor Konnov, Zarko Milosevic, Romain Ruetschi, Josef Widder
A Tendermint Light Client. CoRR (2020)
Igor Konnov, Marijana Lazic, Ilina Stoilkovska, Josef Widder
Tutorial: Parameterized Verification with Byzantine Model Checker. FORTE (2020)
Igor Konnov, Marijana Lazic, Ilina Stoilkovska, Josef Widder
Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker. CoRR (2020)
Sean Braithwaite, Ethan Buchman, Igor Konnov, Zarko Milosevic, Ilina Stoilkovska, Josef Widder, Anca Zamfir
Tendermint Blockchain Synchronization: Formal Specification and Model Checking. ISoLA (1) (2020)
Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger
Eliminating Message Counters in Threshold Automata. ATVA (2020)
Sean Braithwaite, Ethan Buchman, Igor Konnov, Zarko Milosevic, Ilina Stoilkovska, Josef Widder, Anca Zamfir
Formal Specification and Model Checking of the Tendermint Blockchain Synchronization Protocol (Short Paper). FMBC@CAV (2020)
Cezara Dragoi, Josef Widder, Damien Zufferey
Programming at the edge of synchrony. Proc. ACM Program. Lang. 4 (OOPSLA) (2020)
Thanh-Hai Tran, Igor Konnov, Josef Widder
Cutoffs for Symmetric Point-to-Point Distributed Algorithms. NETYS (2020)
Nathalie Bertrand, Igor Konnov, Marijana Lazic, Josef Widder
Verification of Randomized Consensus Algorithms Under Round-Rigid Adversaries. CONCUR (2019)
Andrei Damian, Cezara Dragoi, Alexandru Militaru, Josef Widder
Communication-Closed Asynchronous Protocols. CAV (2) (2019)
Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger
Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking. TACAS (2) (2019)
Benjamin Aminof, Sasha Rubin, Ilina Stoilkovska, Josef Widder, Florian Zuleger
Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction. VMCAI (2018)
Cezara Dragoi, Josef Widder
Reducing asynchrony to synchronized rounds. CoRR (2018)
Jure Kukovec, Igor Konnov, Josef Widder
Reachability in Parameterized Systems: All Flavors of Threshold Automata. CONCUR (2018)
Igor Konnov, Josef Widder
ByMC: Byzantine Model Checker. ISoLA (3) (2018)
Igor V. Konnov, Helmut Veith, Josef Widder
On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability. Inf. Comput. 252 (2017)
Marijana Lazic, Igor Konnov, Josef Widder, Roderick Bloem
Synthesis of Distributed Algorithms with Parameterized Threshold Guards. OPODIS (2017)
Igor V. Konnov, Marijana Lazic, Helmut Veith, Josef Widder
A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms. POPL (2017)
Igor V. Konnov, Josef Widder, Francesco Spegni, Luca Spalazzi
Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms. VMCAI (2017)
Igor Konnov, Marijana Lazic, Helmut Veith, Josef Widder
: parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms. Formal Methods Syst. Des. 51 (2) (2017)
Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, Josef Widder
Decidability in Parameterized Verification. SIGACT News 47 (2) (2016)
Igor Konnov, Marijana Lazic, Helmut Veith, Josef Widder
A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms. CoRR (2016)
Igor Konnov, Helmut Veith, Josef Widder
SMT and POR Beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms. CAV (1) (2015)
Igor V. Konnov, Helmut Veith, Josef Widder
What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms. Ershov Memorial Conference (2015)
Bernadette Charron-Bost, Matthias Függer, Jennifer L. Welch, Josef Widder
Time Complexity of Link Reversal Routing. ACM Trans. Algorithms 11 (3) (2015)
Cezara Dragoi, Thomas A. Henzinger, Helmut Veith, Josef Widder, Damien Zufferey
A Logic-Based Framework for Verifying Consensus Algorithms. VMCAI (2014)
Annu Gmeiner, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder
Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms. SFM (2014)
Srikanth Sastry, Josef Widder
Solvability-Based Comparison of Failure Detectors. NCA (2014)
Igor Konnov, Helmut Veith, Josef Widder
On the Completeness of Bounded Model Checking for Threshold-Based Distributed Algorithms: Reachability. CONCUR (2014)
Srikanth Sastry, Josef Widder
Solvability-Based Comparison of Failure Detectors. CoRR (2014)
Bernadette Charron-Bost, Antoine Gaillard, Jennifer L. Welch, Josef Widder
Link Reversal Routing with Binary Link Labels: Work Complexity. SIAM J. Comput. 42 (2) (2013)
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder
Brief announcement: parameterized model checking of fault-tolerant distributed algorithms by abstraction. PODC (2013)
Bernadette Charron-Bost, Stephan Merz, Andrey Rybalchenko, Josef Widder
Formal Verification of Distributed Algorithms (Dagstuhl Seminar 13141). Dagstuhl Reports 3 (4) (2013)
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder
Parameterized model checking of fault-tolerant distributed algorithms by abstraction. FMCAD (2013)
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder
Towards Modeling and Model Checking Fault-Tolerant Distributed Algorithms. SPIN (2013)
Josef Widder, Martin Biely, Günther Gridling, Bettina Weiss, Jean-Paul Blanquart
Consensus in the presence of mortal Byzantine faulty processes. Distributed Comput. 24 (6) (2012)
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder
Starting a Dialog between Model Checking and Fault-tolerant Distributed Algorithms CoRR (2012)
Matthias Függer, Josef Widder
Efficient Checking of Link-Reversal-Based Concurrent Systems. CONCUR (2012)
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder
Counter Attack on Byzantine Generals: Parameterized Model Checking of Fault-tolerant Distributed Algorithms CoRR (2012)
Srikanth Sastry, Jennifer L. Welch, Josef Widder
Wait-Free Stabilizing Dining Using Regular Registers. OPODIS (2012)
Bernadette Charron-Bost, Matthias Függer, Jennifer L. Welch, Josef Widder
Brief announcement: full reversal routing as a linear dynamical system. SPAA (2011)
Bernadette Charron-Bost, Matthias Függer, Jennifer L. Welch, Josef Widder
Full Reversal Routing as a Linear Dynamical System. SIROCCO (2011)
Bernadette Charron-Bost, Matthias Függer, Jennifer L. Welch, Josef Widder
Partial is Full. SIROCCO (2011)
Bernadette Charron-Bost, Martin Hutle, Josef Widder
In search of lost time. Inf. Process. Lett. 110 (21) (2010)
Martin Biely, Josef Widder
Optimal message-driven implementations of omega with mute processes. ACM Trans. Auton. Adapt. Syst. 4 (1) (2009)
Bernadette Charron-Bost, Jennifer L. Welch, Josef Widder
Link Reversal: How to Play Better to Work Less. ALGOSENSORS (2009)
Josef Widder, Ulrich Schmid
The Theta-Model: achieving synchrony without clocks. Distributed Comput. 22 (1) (2009)
Bernadette Charron-Bost, Antoine Gaillard, Jennifer L. Welch, Josef Widder
Routing without ordering. SPAA (2009)
Emmanuelle Anceaume, Carole Delporte-Gallet, Hugues Fauconnier, Michel Hurfin, Josef Widder
Clock Synchronization in the Byzantine-Recovery Failure Model. OPODIS (2007)
Martin Biely, Martin Hutle, Lucia Draque Penso, Josef Widder
Relating Stabilizing Timing Assumptions to Stabilizing Failure Detectors Regarding Solvability and Efficiency. SSS (2007)
Martin Biely, Josef Widder, Bernadette Charron-Bost, Antoine Gaillard, Martin Hutle, André Schiper
Tolerating corrupted communication. PODC (2007)
Josef Widder, Günther Gridling, Bettina Weiss, Jean-Paul Blanquart
Synchronous Consensus with Mortal Byzantines. DSN (2007)
Josef Widder, Ulrich Schmid
Booting clock synchronization in partially synchronous systems with hybrid process and link failures. Distributed Comput. 20 (2) (2007)
Martin Biely, Josef Widder
Optimal Message-Driven Implementation of Omega with Mute Processes. SSS (2006)
Martin Hutle, Josef Widder
Brief announcement: on the possibility and the impossibility of message-driven self-stabilizing failure detection. PODC (2005)
Martin Hutle, Josef Widder
On the Possibility and the Impossibility of Message-Driven Self-stabilizing Failure Detection. Self-Stabilizing Systems (2005)
Martin Hutle, Josef Widder
Self-Stabilizing Failure Detector Algorithms. Parallel and Distributed Computing and Networks (2005)
Josef Widder, Gérard Le Lann, Ulrich Schmid
Failure Detection with Booting in Partially Synchronous Systems. EDCC (2005)
Jean-François Hermant, Josef Widder
-Model. OPODIS (2005)
Josef Widder
Booting clock Synchronization in Partially Synchronous Systems. DISC (2003)
Chong-Min Kyung, Josef Widder, Dieter A. Mlynski
Adaptive cluster growth: a new algorithm for circuit placement in rectilinear regions. Comput. Aided Des. 24 (1) (1992)
Chong-Min Kyung, Josef Widder, Dieter A. Mlynski
Adaptive Cluster Growth (ACG): a new algorithm for circuit packing in rectilinear region. EURO-DAC (1990)