Josef Widder’s Papers
| 2019 | |
| [60] | Verifying Safety of Synchronous Fault-Tolerant Algorithms Bounded Model Checking Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part II, pages 357-374, 2019. Note: A pre-print including the proofs is available at: https://hal.inria.fr/hal-01925653 |
| 2018 | |
| [59] | Verification of Randomized Distributed Algorithms under Round-Rigid Adversaries HAL, volume hal-01925533, Nov 2018. |
| [58] | Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking HAL, volume hal-01925653, Nov 2018. Note: Accepted at TACAS 2019 |
| [57] | ByMC: Byzantine Model Checker Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems, pages 327-342, 2018, Springer International Publishing. |
| [56] | Reachability in Parameterized Systems: All Flavors of Threshold Automata 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China, pages 19:1-19:17, 2018. |
| [55] | Reducing asynchrony to synchronized rounds arXiv, volume 1804.07078, 2018. |
| [54] | Communication-Closed Layers as Paradigm for Distributed Systems: A Manifesto Sinteza, pages 131-138, 2018. |
| [53] | Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings (Isil Dillig, Jens Palsberg, eds.), volume 10747 of Lecture Notes in Computer Science, pages 1-24, 2018, Springer. |
| 2017 | |
| [52] | Synthesis of Distributed Algorithms with Parameterized Threshold Guards OPODIS, volume 95 of LIPIcs, pages 32:1-32:20, 2017. |
| [51] | Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings, pages 347-366, 2017. |
| [50] | On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability Information and Computation, volume 252, pages 95-109, 2017. |
| [49] | A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms 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 |
| [48] | Para^2: Parameterized Path Reduction, Acceleration, and SMT for Reachability in Threshold-Guarded Distributed Algorithms Formal Methods in System Design, volume 51, number 2, pages 270-307, 2017, Springer. |
| 2016 | |
| [47] | Decidability of Parameterized Verification ACM SIGACT News, volume 47, number 2, pages 53-64, jun 2016. |
| [46] | What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms 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. |
| [45] | A Short Counterexample Property for Safety and Liveness Verification of Fault-Tolerant Distributed Algorithms arXiv/CoRR, volume 1608.05327, 2016. Note: (accepted to POPL 2017) |
| 2015 | |
| [44] | Time Complexity of Link Reversal Routing ACM Trans. Algorithms, volume 11, number 3, pages 18:1-18:39, jan 2015. |
| [43] | Decidability of Parameterized Verification pages 170, 2015. |
| [42] | SMT and POR beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms CAV (Part I), volume 9206 of LNCS, pages 85-102, 2015. |
| 2014 | |
| [41] | Solvability-Based Comparison of Failure Detectors IEEE NCA14, pages 269-276, 2014. |
| [40] | On the Completeness of Bounded Model Checking for Threshold-Based Distributed Algorithms: Reachability Chapter in CONCUR 2014 --- Concurrency Theory (Paolo Baldan, Daniele Gorla, eds.), volume 8704 of Lecture Notes in Computer Science, pages 125-140, 2014. |
| [39] | Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms Formal Methods for Executable Software Models, pages 122-171, 2014, Springer. |
| [38] | A Logic-based Framework for Verifying Consensus Algorithms VMCAI, volume 8318 of LNCS, pages 161-181, 2014. |
| 2013 | |
| [37] | Formal Verification of Distributed Algorithms (Dagstuhl Seminar 13141) 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. |
| [36] | Parameterized model checking of fault-tolerant distributed algorithms by abstraction FMCAD, pages 201-209, 2013. |
| [35] | Towards Modeling and Model Checking Fault-Tolerant Distributed Algorithms SPIN, volume 7976 of LNCS, pages 209-226, 2013. |
| [34] | Brief announcement: parameterized model checking of fault-tolerant distributed algorithms by abstraction PODC, pages 119-121, 2013. |
| [33] | Link Reversal Routing with Binary Link Labels: Work Complexity SIAM Journal on Computing, volume 42, number 2, pages 634-661, 2013. |
| 2012 | |
| [32] | Wait-Free Stabilizing Dining Using Regular Registers OPODIS, volume 7702 of LNCS, pages 284-299, December 2012, Springer. |
| [31] | Starting a Dialog between Model Checking and Fault-tolerant Distributed Algorithms ArXiv e-prints, October 2012. |
| [30] | Counter Attack on Byzantine Generals: Parameterized Model Checking of Fault-tolerant Distributed Algorithms ArXiv e-prints, October 2012. |
| [29] | Consensus in the presence of mortal Byzantine faulty processes Distributed Computing, volume 24, number 6, pages 299-321, 2012. |
| [28] | Who is afraid of Model Checking Distributed Algorithms? 2012, CAV Workshop (EC)\^2. |
| [27] | Efficient Checking of Link-Reversal-Based Concurrent Systems CONCUR, volume 7454 of LNCS, pages 486-499, 2012. |
| 2011 | |
| [26] | On Efficient Checking of Link-reversal-based Concurrent Systems 2011, Unpublished contribution to: (EC)2 2011: Workshop on Exploiting Concurrency Efficiently and Correctly. |
| [25] | Brief Announcement: Full Reversal Routing as a Linear Dynamical System Proceedings of the 23rd ACM Symposium on Parallelism in Algorithms and Architectures (SPAA), pages 129-130, 2011. |
| [24] | Partial is Full Proceedings of the 18th International Colloquium on Structural Information and Communication Complexity (SIROCCO), volume 6796 of LNCS, pages 113-124, 2011, Springer Verlag. |
| [23] | Full Reversal Routing as a Linear Dynamical System Proceedings of the 18th International Colloquium on Structural Information and Communication Complexity (SIROCCO), volume 6796 of LNCS, pages 101-112, 2011, Springer Verlag. |
| 2010 | |
| [22] | In Search of Lost Time Information Processing Letters, volume 110, number 21, pages 928-933, oct 2010. |
| 2009 | |
| [21] | The Theta-Model: Achieving Synchrony without Clocks Distributed Computing, volume 22, number 1, pages 29-47, apr 2009, Springer Verlag. |
| [20] | Link reversal: How to play better to work less Proceedings of the 5th International Workshop on Algorithmic Aspects of Wireless Sensor Networks (Algosensors'09), volume 5304 of LNCS, pages 88-101, 2009. |
| [19] | Routing without Ordering Proceedings of the 21st ACM Symposium on Parallelism in Algorithms and Architectures (SPAA), pages 145-153, 2009. |
| [18] | Optimal Message-Driven Implementations of Omega with Mute Processes ACM Transactions on Autonomous and Adaptive Systems, volume 4, number 1, pages Article 4, 22 pages, 2009, ACM. |
| 2007 | |
| [17] | Clock Synchronization in the Byzantine-Recovery Failure Model International Conference On Principles Of DIstributed Systems OPODIS 2007, pages 90-104, December 2007, Springer Verlag. |
| [16] | Relating Stabilizing Timing Assumptions to Stabilizing Failure Detectors Regarding Solvability and Efficiency 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. |
| [15] | Tolerating Corrupted Communication Proceedings of the 26th ACM Symposium on Principles of Distributed Computing (PODC'07), pages 244-253, August 2007, ACM. |
| [14] | Booting Clock Synchronization in Partially Synchronous Systems with Hybrid Process and Link Failures Distributed Computing, volume 20, number 2, pages 115-140, August 2007, Springer Verlag. |
| [13] | Synchronous Consensus with Mortal Byzantines Proceedings of the International Conference on Dependable Systems and Networks (DSN'07), pages 102-111, June 2007. |
| 2006 | |
| [12] | Optimal Message-Driven Implementation of Omega with Mute Processes 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. |
| [11] | An Efficient Test for a Transistion Signalling based Up-/Down-Counter The Austrian National Conference on the Design of Integrated Circuits and Systems (Austrochip 2006), pages 55-62, October 2006. |
| [10] | Network synchronization in the crash-recovery model 2006, Technical report, Department for Mathematics and Computer Science, University of Mannheim and Technische Universität Wien, Institut für Technische Informatik. |
| [9] | Equivalence of Failure Detectors and Partial Synchony 2006, Technical report, Technische Universität Wien, Institut für Technische Informatik. |
| 2005 | |
| [8] | Implementing Reliable Distributed Real-Time Systems with the Θ-Model Proceedings of the 9th International Conference on Principles of Distributed Systems (OPODIS 2005), volume 3974 of LNCS, pages 334-350, December 2005, Springer Verlag. |
| [7] | On the Possibility and the Impossibility of Message-Driven Self-Stabilizing Failure Detection Proceedings of the Seventh International Symposium on Self Stabilizing Systems (SSS 2005), volume 3764 of LNCS, pages 153-170, October 2005, Springer Verlag. |
| [6] | Brief Announcement: On the Possibility and the Impossibility of Message-Driven Self-Stabilizing Failure Detection Proceedings of the 24th ACM Symposium on Principles of Distributed Computing (PODC'05), pages 208, July 2005. |
| [5] | Failure Detection with Booting in Partially Synchronous Systems Proceedings of the 5th European Dependable Computing Conference (EDCC-5), volume 3463 of LNCS, pages 20-37, April 2005, Springer Verlag. |
| [4] | Self-Stabilizing Failure Detector Algorithms Proc. IASTED International Conference on Parallel and Distributed Computing and Networks (PDCN'05), pages 485-490, February 2005, IASTED/ACTA Press. |
| 2004 | |
| [3] | Distributed Computing in the Presence of Bounded Asynchrony pages 117 pages, May 2004, PhD thesis, Vienna University of Technology, Fakultät für Informatik. |
| 2003 | |
| [2] | Booting Clock Synchronization in Partially Synchronous Systems Proceedings of the 17th International Symposium on Distributed Computing (DISC'03), volume 2848 of LNCS, pages 121-135, October 2003, Springer Verlag. |
| 2002 | |
| [1] | Switching On. How Processes Initialize for Consistent Broadcast pages 32 pages, October 2002, Master's thesis, Technische Universität Wien, Department of Automation. |
