Josef Widder’s Papers

2017
[51] Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms
Igor V. Konnov, Josef Widder, Francesco Spegni, Luca Spalazzi
Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings, pages 347-366, 2017.
[bibtex] [pdf] [doi]
[50] On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability
Igor V. Konnov, Helmut Veith, Josef Widder
Information and Computation, volume 252, pages 95-109, 2017.
[bibtex] [pdf] [doi]
[49] A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms
Igor V. Konnov, Marijana Lazic, Helmut Veith, Josef Widder
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 719-734, 2017.
Note: A pre-print including the proofs is available at http://arxiv.org/abs/1608.05327
[bibtex] [pdf]
[48]Para^2: Parameterized Path Reduction, Acceleration, and SMT for Reachability in Threshold-Guarded Distributed Algorithms
Igor Konnov, Marijana Lazic, Helmut Veith, Josef Widder
Formal Methods in System Design, 2017, Springer.
Note: to appear
[bibtex]
2016
[47] Decidability of Parameterized Verification
Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, Josef Widder
ACM SIGACT News, volume 47, number 2, pages 53-64, jun 2016.
[bibtex] [pdf]
[46] What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms
Igor Konnov, Helmut Veith, Josef Widder
Perspectives of System Informatics: 10th International Andrei Ershov Informatics Conference, PSI 2015, in Memory of Helmut Veith, Kazan and Innopolis, Russia, August 24-27, 2015, Revised Selected Papers (Manuel Mazzara, Andrei Voronkov, eds.), volume 9609 of LNCS, pages 6-21, 2016, Springer International Publishing.
[bibtex] [pdf]
[45] A Short Counterexample Property for Safety and Liveness Verification of Fault-Tolerant Distributed Algorithms
Igor Konnov, Marijana Lazic, Helmut Veith, Josef Widder
arXiv/CoRR, volume 1608.05327, 2016.
Note: (accepted to POPL 2017)
[bibtex] [pdf]
2015
[44] Time Complexity of Link Reversal Routing
Bernadette Charron-Bost, Matthias Függer, Jennifer L. Welch, Josef Widder
ACM Trans. Algorithms, volume 11, number 3, pages 18:1-18:39, jan 2015.
[bibtex] [pdf] [doi]
[43] Decidability of Parameterized Verification
Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, Josef Widder
pages 170, 2015.
[bibtex] [pdf] [doi]
[42] SMT and POR beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms
Igor Konnov, Helmut Veith, Josef Widder
CAV (Part I), volume 9206 of LNCS, pages 85-102, 2015.
[bibtex] [pdf]
2014
[41] Solvability-Based Comparison of Failure Detectors
Srikanth Sastry, Josef Widder
IEEE NCA14, pages 269-276, 2014.
[bibtex] [pdf]
[40] On the Completeness of Bounded Model Checking for Threshold-Based Distributed Algorithms: Reachability
Igor Konnov, Helmut Veith, Josef Widder
Chapter in CONCUR 2014 --- Concurrency Theory (Paolo Baldan, Daniele Gorla, eds.), volume 8704 of Lecture Notes in Computer Science, pages 125-140, 2014.
[bibtex] [pdf]
[39] Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms
Annu Gmeiner, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder
Formal Methods for Executable Software Models, pages 122-171, 2014, Springer.
[bibtex] [pdf]
[38] A Logic-based Framework for Verifying Consensus Algorithms
Cezara Drăgoi, Thomas A. Henzinger, Helmut Veith, Josef Widder, Damien Zufferey
VMCAI, volume 8318 of LNCS, pages 161-181, 2014.
[bibtex] [pdf]
2013
[37] Formal Verification of Distributed Algorithms (Dagstuhl Seminar 13141)
Bernadette Charron-Bost, Stephan Merz, Andrey Rybalchenko, Josef Widder
Dagstuhl Reports (Bernadette Charron-Bost, Stepahn Merz, Andrey Rybalchenko, Josef Widder, eds.), volume 3, number 4, pages 1-16, 2013, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik.
[bibtex] [pdf] [doi]
[36] Parameterized model checking of fault-tolerant distributed algorithms by abstraction
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder
FMCAD, pages 201-209, 2013.
[bibtex] [pdf]
[35] Towards Modeling and Model Checking Fault-Tolerant Distributed Algorithms
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder
SPIN, volume 7976 of LNCS, pages 209-226, 2013.
[bibtex] [pdf]
[34] Brief announcement: parameterized model checking of fault-tolerant distributed algorithms by abstraction
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder
PODC, pages 119-121, 2013.
[bibtex] [pdf]
[33] Link Reversal Routing with Binary Link Labels: Work Complexity
Bernadette Charron-Bost, Antoine Gaillard, Jennifer Welch, Josef Widder
SIAM Journal on Computing, volume 42, number 2, pages 634-661, 2013.
[bibtex] [pdf]
2012
[32] Wait-Free Stabilizing Dining Using Regular Registers
Srikanth Sastry, Jennifer L. Welch, Josef Widder
OPODIS, volume 7702 of LNCS, pages 284-299, December 2012, Springer.
[bibtex] [pdf]
[31] Starting a Dialog between Model Checking and Fault-tolerant Distributed Algorithms
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder
ArXiv e-prints, October 2012.
[bibtex] [pdf]
[30] Counter Attack on Byzantine Generals: Parameterized Model Checking of Fault-tolerant Distributed Algorithms
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder
ArXiv e-prints, October 2012.
[bibtex] [pdf]
[29] Consensus in the presence of mortal Byzantine faulty processes
Josef Widder, Martin Biely, Günther Gridling, Bettina Weiss, Jean-Paul Blanquart
Distributed Computing, volume 24, number 6, pages 299-321, 2012.
[bibtex] [pdf]
[28] Who is afraid of Model Checking Distributed Algorithms?
Igor Konnov, Helmut Veith, Josef Widder
2012, CAV Workshop (EC)\^2.
[bibtex] [pdf]
[27] Efficient Checking of Link-Reversal-Based Concurrent Systems
Matthias Függer, Josef Widder
CONCUR, volume 7454 of LNCS, pages 486-499, 2012.
[bibtex] [pdf]
2011
[26] On Efficient Checking of Link-reversal-based Concurrent Systems
Matthias Függer, Josef Widder
2011, Unpublished contribution to: (EC)2 2011: Workshop on Exploiting Concurrency Efficiently and Correctly.
[bibtex] [pdf]
[25] Brief Announcement: Full Reversal Routing as a Linear Dynamical System
Bernadette Charron-Bost, Matthias Függer, Jennifer L. Welch, Josef Widder
Proceedings of the 23rd ACM Symposium on Parallelism in Algorithms and Architectures (SPAA), pages 129-130, 2011.
[bibtex] [pdf]
[24] Partial is Full
Bernadette Charron-Bost, Matthias Függer, Jennifer L. Welch, Josef Widder
Proceedings of the 18th International Colloquium on Structural Information and Communication Complexity (SIROCCO), volume 6796 of LNCS, pages 113-124, 2011, Springer Verlag.
[bibtex] [pdf]
[23] Full Reversal Routing as a Linear Dynamical System
Bernadette Charron-Bost, Matthias Függer, Jennifer L. Welch, Josef Widder
Proceedings of the 18th International Colloquium on Structural Information and Communication Complexity (SIROCCO), volume 6796 of LNCS, pages 101-112, 2011, Springer Verlag.
[bibtex] [pdf]
2010
[22] In Search of Lost Time
Bernadette Charron-Bost, Martin Hutle, Josef Widder
Information Processing Letters, volume 110, number 21, pages 928-933, oct 2010.
[bibtex] [pdf]
2009
[21] The Theta-Model: Achieving Synchrony without Clocks
Josef Widder, Ulrich Schmid
Distributed Computing, volume 22, number 1, pages 29-47, apr 2009, Springer Verlag.
[bibtex] [pdf]
[20] Link reversal: How to play better to work less
Bernadette Charron-Bost, Jennifer L. Welch, Josef Widder
Proceedings of the 5th International Workshop on Algorithmic Aspects of Wireless Sensor Networks (Algosensors'09), volume 5304 of LNCS, pages 88-101, 2009.
[bibtex] [pdf]
[19] Routing without Ordering
Bernadette Charron-Bost, Antoine Gaillard, Jennifer L. Welch, Josef Widder
Proceedings of the 21st ACM Symposium on Parallelism in Algorithms and Architectures (SPAA), pages 145-153, 2009.
[bibtex] [pdf]
[18] Optimal Message-Driven Implementations of Omega with Mute Processes
Martin Biely, Josef Widder
ACM Transactions on Autonomous and Adaptive Systems, volume 4, number 1, pages Article 4, 22 pages, 2009, ACM.
[bibtex] [pdf]
2007
[17] Clock Synchronization in the Byzantine-Recovery Failure Model
Emmanuelle Anceaume, Carole Delporte-Gallet, Hugues Fauconnier, Michel Hurfin, Josef Widder
International Conference On Principles Of DIstributed Systems OPODIS 2007, pages 90-104, December 2007, Springer Verlag.
[bibtex] [pdf]
[16] Relating Stabilizing Timing Assumptions to Stabilizing Failure Detectors Regarding Solvability and Efficiency
Martin Biely, Martin Hutle, Lucia Draque Penso, Josef Widder
9th International Symposium on Stabilization, Safety, and Security of Distributed Systems, volume 4838 of Lecture Notes in Computer Science, pages 4-20, November 2007, Springer Verlag.
[bibtex] [pdf]
[15] Booting Clock Synchronization in Partially Synchronous Systems with Hybrid Process and Link Failures
Josef Widder, Ulrich Schmid
Distributed Computing, volume 20, number 2, pages 115-140, August 2007, Springer Verlag.
[bibtex] [pdf]
[14] Tolerating Corrupted Communication
Martin Biely, Bernadette Charron-Bost, Antoine Gaillard, Martin Hutle, André Schiper, Josef Widder
Proceedings of the 26th ACM Symposium on Principles of Distributed Computing (PODC'07), pages 244-253, August 2007, ACM.
[bibtex] [pdf]
[13] Synchronous Consensus with Mortal Byzantines
Josef Widder, Günther Gridling, Bettina Weiss, Jean-Paul Blanquart
Proceedings of the International Conference on Dependable Systems and Networks (DSN'07), pages 102-111, June 2007.
[bibtex] [pdf]
2006
[12] Optimal Message-Driven Implementation of Omega with Mute Processes
Martin Biely, Josef Widder
Proceedings of the Eighth International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2006), volume 4280 of LNCS, pages 110-121, November 2006, Springer Verlag.
[bibtex] [pdf]
[11] An Efficient Test for a Transistion Signalling based Up-/Down-Counter
Matthias Függer, Thomas Handl, Andreas Steininger, Josef Widder, Christian Tögel
The Austrian National Conference on the Design of Integrated Circuits and Systems (Austrochip 2006), pages 55-62, October 2006.
[bibtex] [pdf]
[10] Network synchronization in the crash-recovery model
Felix C. Freiling, Sven Henkel, Josef Widder
2006, Technical report, Department for Mathematics and Computer Science, University of Mannheim and Technische Universität Wien, Institut für Technische Informatik.
[bibtex] [pdf]
[9] Equivalence of Failure Detectors and Partial Synchony
Felix Freiling, Martin Hutle, Lucia Penso, Josef Widder
2006, Technical report, Technische Universität Wien, Institut für Technische Informatik.
[bibtex] [pdf]
2005
[8] Implementing Reliable Distributed Real-Time Systems with the Θ-Model
Jean-François Hermant, Josef Widder
Proceedings of the 9th International Conference on Principles of Distributed Systems (OPODIS 2005), volume 3974 of LNCS, pages 334-350, December 2005, Springer Verlag.
[bibtex] [pdf]
[7] On the Possibility and the Impossibility of Message-Driven Self-Stabilizing Failure Detection
Martin Hutle, Josef Widder
Proceedings of the Seventh International Symposium on Self Stabilizing Systems (SSS 2005), volume 3764 of LNCS, pages 153-170, October 2005, Springer Verlag.
[bibtex] [pdf]
[6] Brief Announcement: On the Possibility and the Impossibility of Message-Driven Self-Stabilizing Failure Detection
Martin Hutle, Josef Widder
Proceedings of the 24th ACM Symposium on Principles of Distributed Computing (PODC'05), pages 208, July 2005.
[bibtex] [pdf]
[5] Failure Detection with Booting in Partially Synchronous Systems
Josef Widder, Gérard Le Lann, Ulrich Schmid
Proceedings of the 5th European Dependable Computing Conference (EDCC-5), volume 3463 of LNCS, pages 20-37, April 2005, Springer Verlag.
[bibtex] [pdf]
[4] Self-Stabilizing Failure Detector Algorithms
Martin Hutle, Josef Widder
Proc. IASTED International Conference on Parallel and Distributed Computing and Networks (PDCN'05), pages 485-490, February 2005, IASTED/ACTA Press.
[bibtex] [pdf]
2004
[3] Distributed Computing in the Presence of Bounded Asynchrony
Josef Widder
pages 117 pages, May 2004, PhD thesis, Vienna University of Technology, Fakultät für Informatik.
[bibtex] [pdf]
2003
[2] Booting Clock Synchronization in Partially Synchronous Systems
Josef Widder
Proceedings of the 17th International Symposium on Distributed Computing (DISC'03), volume 2848 of LNCS, pages 121-135, October 2003, Springer Verlag.
[bibtex] [pdf]
2002
[1] Switching On. How Processes Initialize for Consistent Broadcast
Josef Widder
pages 32 pages, October 2002, Master's thesis, Technische Universität Wien, Department of Automation.
[bibtex] [pdf]

Latest News

Helmut Veith Stipend 2017: Deadline Extension (November 30)

The application deadline for the Helmut Veith Stipend 2017 has been extended to November 30. The stipend is dedicated to the memory of an outstanding computer scientist who worked in the fields of logic in computer science, computer-aided verification, software engineering, and computer security. We encourage all female master’s students attending (or planning to attend) […]

Continue reading

Helmut Veith Stipend 2017

Outstanding female students in the field of computer science who pursue (or plan to pursue) one of the master‘s programs in Computer Science at TU Wien taught in English are invited to apply for the Helmut Veith Stipend

Continue reading

Helmut Veith Stipend

The first recipient of the Helmut Veith Stipend for excellent female master’s students in computer science will be presented on March 14 at the following event: "More female students in computer science. Who cares?" Panel discussion with renowned scientists about diversity in STEM Studies March 14, 5:30pm, TU Wien The Helmut Veith Stipend is dedicated […]

Continue reading

WAIT 2016 in Vienna

The third WAIT workshop on induction is held between 17-18 November at the TU Wien. Details are available on the workshop page.

Continue reading

Full news archive