2023S

• Introduction to Logical Methods in Computer Science / 184.766 / VO
• Research Seminar LogiCS / 184.767 / SE

• Tools for Concurrent and distributed Systems
  2011 – 2019 / Austrian Science Fund (FWF) / Publication: 57366
• Proof Seeding for Software Verification
  2011 – 2015 / Vienna Science and Technology Fund (WWTF) / Publications: 57366, 59881
• Asynchronous Distributed Algorithms in the Theta-Model
  2004 – 2008 / Austrian Science Fund (FWF) / Publication: 57162
• Automated proof based System and Software Engineering for Real-Time Applications
  2004 – 2008 / European Commission

Note: Due to the rollout of TU Wien’s new publication database, the list below may be slightly outdated. Once the migration is complete, everything will be up to date again.

2022

• Verifying safety of synchronous fault-tolerant algorithms by bounded model checking / Stoilkovska, I., Konnov, I., Widder, J., & Zuleger, F. (2022). Verifying safety of synchronous fault-tolerant algorithms by bounded model checking. International Journal on Software Tools for Technology Transfer, 24(1), 33–48. https://doi.org/10.1007/s10009-021-00637-9

2021

• Eliminating Message Counters in Synchronous Threshold Automata / Stoilkovska, I., Konnov, I., Widder, J., & Zuleger, F. (2021). Eliminating Message Counters in Synchronous Threshold Automata. In Lecture Notes in Computer Science (pp. 196–218). Springer LNCS. https://doi.org/10.1007/978-3-030-67067-2_10

2020

• Eliminating Message Counters in Threshold Automata / Stoilkovska, I., Konnov, I., Widder, J., & Zuleger, F. (2020). Eliminating Message Counters in Threshold Automata. In Automated Technology for Verification and Analysis. 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings (pp. 192–212). Springer. https://doi.org/10.34726/423
• Tutorial: Parameterized Verification with Byzantine Model Checker

2019

• Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking / Stoilkovska, I., Konnov, I., Widder, J., & Zuleger, F. (2019). Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (pp. 357–374). Springer. http://hdl.handle.net/20.500.12708/56804
• Verification of Randomized Consensus Algorithms Under Round-Rigid Adversaries / Bertrand, N., Konnov, I., Lazić, M., & Widder, J. (2019). Verification of Randomized Consensus Algorithms Under Round-Rigid Adversaries. In 30th International Conference on Concurrency Theory (pp. 33:1-33:15). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany. https://doi.org/10.4230/LIPIcs.CONCUR.2019.33
• Communication-Closed Asynchronous Protocols / Damian, A., Drăgoi, C., Militaru, A., & Widder, J. (2019). Communication-Closed Asynchronous Protocols. In Computer Aided Verification (pp. 344–363). Springer. https://doi.org/10.1007/978-3-030-25543-5_20

2018

• Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction / Aminof, B., Rubin, S., Stoilkovska, I., Widder, J., & Zuleger, F. (2018). Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction. In Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings ; Dillig, Isil; Palsberg, Jens. Cham. https://doi.org/10.1007/978-3-319-73721-8_1
• 32nd International Symposium on Distributed Computing / Schmid, U., & Widder, J. (Eds.). (2018). 32nd International Symposium on Distributed Computing. Dagstuhl Publishing LIPICS. https://doi.org/10.4230/LIPIcs.DISC.2018.0
• Reachability in Parameterized Systems: All Flavors of Threshold Automata / Kukovec, J., Konnov, I., & Widder, J. (2018). Reachability in Parameterized Systems: All Flavors of Threshold Automata. In 29th International Conference on Concurrency Theory (CONCUR 2018) (pp. 19:1-19:17). Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.CONCUR.2018.19
• ByMC: Byzantine Model Checker / Konnov, I., & Widder, J. (2018). ByMC: Byzantine Model Checker. In Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems (pp. 327–342). Lecture Notes in Computer Science. Springer Verlag. https://doi.org/10.1007/978-3-030-03424-5_22
• Communication-Closed Layers as Paradigm for Distributed Systems: A Manifesto / Dragoi, C., Lazić, M., & Widder, J. (2018). Communication-Closed Layers as Paradigm for Distributed Systems: A Manifesto. In Proceedings of the International Scientific Conference - Sinteza 2018. Sinteza 2018 International Scientific Conference on Information Technology and Data Related Research, Belgrad, Serbien, Non-EU. Singidunum University. https://doi.org/10.15308/sinteza-2018-131-138

2017

• Para^2: Parameterized Path Reduction, Acceleration, and SMT for Reachability in Threshold-Guarded Distributed Algorithms / Konnov, I., Lazić, M., Veith, H., & Widder, J. (2017). Para^2: Parameterized Path Reduction, Acceleration, and SMT for Reachability in Threshold-Guarded Distributed Algorithms. Formal Methods in System Design, 51(2), 270–307. https://doi.org/10.1007/s10703-017-0297-4
• On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability / Konnov, I., Veith, H., & Widder, J. (2017). On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability. Information and Computation, 252, 95–109. https://doi.org/10.1016/j.ic.2016.03.006
• Synthesis of Distributed Algorithms with Parameterized Threshold Guards / Lazić, M., Konnov, I., Widder, J., & Bloem, R. (2017). Synthesis of Distributed Algorithms with Parameterized Threshold Guards. In OPODIS (pp. 32:1-32:20). LIPIcs-Leibniz International Proceedings in Informatics. https://doi.org/10.4230/LIPIcs.OPODIS.2017.32
• A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms / Konnov, I., Lazić, M., Veith, H., & Widder, J. (2017). A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), Paris, France, EU. ACM. https://doi.org/10.1145/3009837.3009860

2016

• Decidability of Parameterized Verification / Bloem, R., Jacobs, S., Khalimov, A., Konnov, I., Rubin, S., Veith, H., & Widder, J. (2016). Decidability of Parameterized Verification. ACM SIGACT News, 47(2), 53–64. https://doi.org/10.1145/2951860.2951873
• Model Checking of Threshold-based Fault-Tolerant Distributed Algorithms / Lazić, M., Konnov, I., Veith, H., & Widder, J. (2016). Model Checking of Threshold-based Fault-Tolerant Distributed Algorithms. 7th Workshop on Program Semantics, Specification and Verification: Theory and Applications, St. Petersburg, Russia, Non-EU. http://hdl.handle.net/20.500.12708/86426
• Parameterized Verification of Liveness of Distributed Algorithms / Konnov, I., Lazić, M., Veith, H., & Widder, J. (2016). Parameterized Verification of Liveness of Distributed Algorithms. Workshop on Formal Reasoning in Distributed Algorithms (FRiDA), Wien, Austria. http://hdl.handle.net/20.500.12708/86425

2015

• Time Complexity of Link Reversal Routing / Charron-Bost, B., Függer, M., Welch, J. L., & Widder, J. (2015). Time Complexity of Link Reversal Routing. ACM Transactions on Algorithms, 11(3), 1–39. https://doi.org/10.1145/2644815
• SMT and POR Beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms / Konnov, I., Veith, H., & Widder, J. (2015). SMT and POR Beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms. In Computer Aided Verification (pp. 85–102). LNCS Springer. https://doi.org/10.1007/978-3-319-21690-4_6
• Decidability of Parameterized Verification / Bloem, R., Jacobs, S., Khalimov, A., Konnov, I., Rubin, S., Veith, H., & Widder, J. (2015). Decidability of Parameterized Verification. In Synthesis Lectures on Distributed Computing Theory (p. 170). Morgan & Claypool Publishers. https://doi.org/10.2200/s00658ed1v01y201508dct013

2014

• Approaching Verification and Validation Challenges in Smart Grids / Deutsch, T., & Widder, J. (2014). Approaching Verification and Validation Challenges in Smart Grids. In Tagungsband ComForEn 2014 (p. 6). Eigenverlag des Österreich isch en Verbandes für Elektrotec h nik. http://hdl.handle.net/20.500.12708/55738
• A Logic-Based Framework for Verifying Consensus Algorithms / Drăgoi, C., Henzinger, T. A., Veith, H., Widder, J., & Zufferey, D. (2014). A Logic-Based Framework for Verifying Consensus Algorithms. In Lecture Notes in Computer Science (pp. 161–181). Springer / LNCS. https://doi.org/10.1007/978-3-642-54013-4_10
• On the Completeness of Bounded Model Checking for Threshold-Based Distributed Algorithms: Reachability / Konnov, I., Veith, H., & Widder, J. (2014). On the Completeness of Bounded Model Checking for Threshold-Based Distributed Algorithms: Reachability. In CONCUR 2014 – Concurrency Theory (pp. 125–140). https://doi.org/10.1007/978-3-662-44584-6_10
• Solvability-Based Comparison of Failure Detectors / Sastry, S., & Widder, J. (2014). Solvability-Based Comparison of Failure Detectors. In 2014 IEEE 13th International Symposium on Network Computing and Applications. International Symposium on Network Computing and Applications (NCA), Boston, MA, USA, Non-EU. IEEE Computer Society. https://doi.org/10.1109/nca.2014.46
• Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms / Gmeiner, A., Konnov, I., Schmid, U., Veith, H., & Widder, J. (2014). Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms. In Lecture Notes in Computer Science (pp. 122–171). Springer. https://doi.org/10.1007/978-3-319-07317-0_4

2013

• Link Reversal Routing with Binary Link Labels: Work Complexity / Charron-Bost, B., Gaillard, A., Welch, J. L., & Widder, J. (2013). Link Reversal Routing with Binary Link Labels: Work Complexity. SIAM Journal on Computing, 42(2), 634–661. https://doi.org/10.1137/110843095
• Formal Verification of Distributed Algorithms / Charron-Bost, B., Merz, S., Rybalchenko, A., & Widder, J. (Eds.). (2013). Formal Verification of Distributed Algorithms. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany. https://doi.org/10.4230/DagRep.3.4.1
• Brief announcement / John, A., Konnov, I., Schmid, U., Veith, H., & Widder, J. (2013). Brief announcement. In Proceedings of the 2013 ACM symposium on Principles of distributed computing - PODC ’13. ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing (PODC), Montreal, Kanada, Non-EU. ACM. https://doi.org/10.1145/2484239.2484285
• Parameterized model checking of fault-tolerant distributed algorithms by abstraction / John, A., Konnov, I., Schmid, U., Veith, H., & Widder, J. (2013). Parameterized model checking of fault-tolerant distributed algorithms by abstraction. In FMCAD (pp. 201–209). http://hdl.handle.net/20.500.12708/54827
• Towards Modeling and Model Checking Fault-Tolerant Distributed Algorithms / John, A., Konnov, I., Schmid, U., Veith, H., & Widder, J. (2013). Towards Modeling and Model Checking Fault-Tolerant Distributed Algorithms. In Model Checking Software (pp. 209–226). LNCS, Springer. https://doi.org/10.1007/978-3-642-39176-7_14

2012

• Consensus in the presence of mortal Byzantine faulty processes / Widder, J., Biely, M., Gridling, G., Weiss, B., & Blanquart, J.-P. (2012). Consensus in the presence of mortal Byzantine faulty processes. Distributed Computing, 24(6), 299–321. https://doi.org/10.1007/s00446-011-0147-3
• Who is afraid of Model Checking Distributed Algorithms? / Konnov, I., Veith, H., & Widder, J. (2012). Who is afraid of Model Checking Distributed Algorithms? Workshop on Exploiting Concurrency Efficiently and Correctly, Berkeley, CA, USA, Non-EU. http://hdl.handle.net/20.500.12708/85358
• Who is afraid of Model Checking Distributed Algorithms? / John, A., Konnov, I., Schmid, U., Veith, H., & Widder, J. (2012). Who is afraid of Model Checking Distributed Algorithms? PUMA/RISE Seminar, Traunkirchen, Austria. http://hdl.handle.net/20.500.12708/85435
• Parameterized Model Checking of Fault-tolerant Distributed Algorithms / John, A., Konnov, I., Schmid, U., Veith, H., & Widder, J. (2012). Parameterized Model Checking of Fault-tolerant Distributed Algorithms. Dagstuhl Seminar 12461: Games and Decisions for Rigorous Systems Engineering, Dagstuhl, Deutschland, EU. http://hdl.handle.net/20.500.12708/85432
• Counter Attack against Byzantine Generals / John, A., Konnov, I., Schmid, U., Veith, H., & Widder, J. (2012). Counter Attack against Byzantine Generals. Alpine Verification Meeting, IST Austria, Austria. http://hdl.handle.net/20.500.12708/85359
• Wait-Free Stabilizing Dining Using Regular Registers / Sastry, S., Welch, J. L., & Widder, J. (2012). Wait-Free Stabilizing Dining Using Regular Registers. In Lecture Notes in Computer Science (pp. 284–299). LNCS / Springer. https://doi.org/10.1007/978-3-642-35476-2_20
• Efficient Checking of Link-Reversal-Based Concurrent Systems / Függer, M., & Widder, J. (2012). Efficient Checking of Link-Reversal-Based Concurrent Systems. In Lecture Notes in Computer Science (pp. 486–499). Lecture Notes in Computer Science. Springer Verlag. https://doi.org/10.1007/978-3-642-32940-1_34

2011

• On Efficient Checking of Link-reversal-based Concurrent Systems / Függer, M., & Widder, J. (2011). On Efficient Checking of Link-reversal-based Concurrent Systems. PUMA/RISE Seminar, Traunkirchen, Austria. http://hdl.handle.net/20.500.12708/85311

2010

• In search of lost time / Charron-Bost, B., Hutle, M., & Widder, J. (2010). In search of lost time. Information Processing Letters, 110(21), 928–933. https://doi.org/10.1016/j.ipl.2010.07.017

2009

• Optimal Message-Driven Implementations of Omega with Mute Processes / Widder, J., & Biely, M. (2009). Optimal Message-Driven Implementations of Omega with Mute Processes. ACM Transactions on Autonomous and Adaptive Systems, 4(1). https://doi.org/10.1145/1462187
• The Theta-Model: achieving synchrony without clocks / Widder, J., & Schmid, U. (2009). The Theta-Model: achieving synchrony without clocks. Distributed Computing, 22(1), 29–47. https://doi.org/10.1007/s00446-009-0080-x
• Link Reversal: How to Play Better to Work Less / Charron-Bost, B., Welch, J. L., & Widder, J. (2009). Link Reversal: How to Play Better to Work Less. In Algorithmic Aspects of Wireless Sensor Networks (pp. 88–101). Springer. https://doi.org/10.1007/978-3-642-05434-1_10
• Routing without ordering / Charron-Bost, B., Gaillard, A., Welch, J., & Widder, J. (2009). Routing without ordering. In Proceedings of the twenty-first annual symposium on Parallelism in algorithms and architectures - SPAA ’09. SPAA 2009 (Parallelism in Algorithms and Architectures), Calgary, Alberta, Canada, Non-EU. ACM. https://doi.org/10.1145/1583991.1584034

2007

• Clock Synchronization in the Byzantine-Recovery Failure Model / Anceaume, E., Delporte-Gallet, C., Fauconnier, H., Hurfin, M., & Widder, J. (2007). Clock Synchronization in the Byzantine-Recovery Failure Model. In International Conference On Principles Of DIstributed System (pp. 90–104). http://hdl.handle.net/20.500.12708/52073
• Synchronous Consensus with Mortal Byzantines / Widder, J., Gridling, G., Weiss, B., & Blanquart, J.-P. (2007). Synchronous Consensus with Mortal Byzantines. In Proceedings of the 37th Annual IEEE/IFIP International Conference on Dependable Systems and Networks. IEEE Conference on Dependable Systems and Networks (DSN), Philadelphia, PA, USA, Non-EU. http://hdl.handle.net/20.500.12708/52033
• Relating Stabilizing Timing Assumptions to Stabilizing Failure Detectors Regarding Solvability and Efficiency / Biely, M., Hutle, M., Penso, L. D., & Widder, J. (2007). Relating Stabilizing Timing Assumptions to Stabilizing Failure Detectors Regarding Solvability and Efficiency. In stabilization. Ninth International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2007), Paris, EU. http://hdl.handle.net/20.500.12708/52032
• Tolerating Corrupted Communication / Biely, M., Charron-Bost, B., Gaillard, A., Hutle, M., Schiper, A., & Widder, J. (2007). Tolerating Corrupted Communication. In 26th ACM Symposium on Principles of Distributed Computing (PODC’07) (pp. 244–253). http://hdl.handle.net/20.500.12708/52017
• Booting Clock Synchronization in Partially Synchronous Systems with Hybrid Process and Link Failures / Widder, J., & Schmid, U. (2007). Booting Clock Synchronization in Partially Synchronous Systems with Hybrid Process and Link Failures. In Distributed Computing (pp. 115–140). Springer-Verlag. http://hdl.handle.net/20.500.12708/25412

2006

• Synchronous Consensus with Mortal Byzantines / Widder, J., Gridling, G., Weiss, B., & Blanquart, J.-P. (2006). Synchronous Consensus with Mortal Byzantines. Dagstuhl Seminar 06371. From Security to Dependability, Dagstuhl, EU. http://hdl.handle.net/20.500.12708/84588
• Simulating Distributed Real-Time Systems / Albeseder, D., & Widder, J. (2006). Simulating Distributed Real-Time Systems. In Junior Scientist Conference 2006 (pp. 83–84). http://hdl.handle.net/20.500.12708/51573
• Optimal Message-Driven Implementations of Omega with Mute Processes / Biely, M., & Widder, J. (2006). Optimal Message-Driven Implementations of Omega with Mute Processes. In Stabilization, Safety, and Security of Distributed Systems (pp. 110–121). http://hdl.handle.net/20.500.12708/51523
• An Efficient Test for a Transition Signalling based Up-/Down-Counter / Függer, M., Handl, T., Steininger, A., Widder, J., & Tögel, C. (2006). An Efficient Test for a Transition Signalling based Up-/Down-Counter. In Austrochip Mikroelektroniktagung (pp. 55–62). http://hdl.handle.net/20.500.12708/51505 / Project: DARTS

2005

• Implementing Reliable Distributed Real Time Systems with the Theta Model / Hermant, J.-F., & Widder, J. (2005). Implementing Reliable Distributed Real Time Systems with the Theta Model. In 9th International Conference on Principles of Distributed Systems (pp. 259–271). http://hdl.handle.net/20.500.12708/51175
• Brief Announcement: On the Possibility and the Impossibility of Message-Driven Self-Stabilizing Failure Detection / Hutle, M., & Widder, J. (2005). Brief Announcement: On the Possibility and the Impossibility of Message-Driven Self-Stabilizing Failure Detection. In Proceedings of the 24th ACM Symposium on Principles of Distributed Computing (p. 208). http://hdl.handle.net/20.500.12708/51124
• Failure Detection with Booting in Partially Synchronous Systems / Widder, J., Le Lann, G., & Schmid, U. (2005). Failure Detection with Booting in Partially Synchronous Systems. In Dependable Computing Conference - EDCC5 (pp. 20–37). http://hdl.handle.net/20.500.12708/51123
• On the Possibility and the Impossibility of Message-Driven Self-Stabilizing Failure Detection / Hutle, M., & Widder, J. (2005). On the Possibility and the Impossibility of Message-Driven Self-Stabilizing Failure Detection. In Self Stabilizing Systems (pp. 153–170). http://hdl.handle.net/20.500.12708/51122
• Self-Stabilizing Failure Detector Algorithms / Hutle, M., & Widder, J. (2005). Self-Stabilizing Failure Detector Algorithms. In IASTED International Conference on Parallel and Distributed Computing and Networks (pp. 485–490). http://hdl.handle.net/20.500.12708/51119

2004

• Distributed computing in the presence of bounded asynchrony / Widder, J. (2004). Distributed computing in the presence of bounded asynchrony [Dissertation, Technische Universität Wien]. reposiTUm. https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-13246
• Why, Where and How to Use the Theta-Model / Widder, J. (2004). Why, Where and How to Use the Theta-Model. Seminaire Reflecs in INRIA Rocquencourt, Frankreich, INRIA Rocquencourt, Frankreich, Austria. http://hdl.handle.net/20.500.12708/84388
• VLSI Design and the Theta-Model (Kurzvorstellungen aktueller Forschung) / Widder, J. (2004). VLSI Design and the Theta-Model (Kurzvorstellungen aktueller Forschung). Diskussionskreis Fehlertoleranz, Berlin, Austria. http://hdl.handle.net/20.500.12708/84387
• The Theta-Model, and how to Boot Clock Synchronization in it / Widder, J. (2004). The Theta-Model, and how to Boot Clock Synchronization in it. Seminaire Reflecs in INRIA Rocquencourt, Frankreich, INRIA Rocquencourt, Frankreich, Austria. http://hdl.handle.net/20.500.12708/84385
• On the Possibility and the Impossibility of Time Free Self-Stabilizing Failure Detection / Hutle, M., & Widder, J. (2004). On the Possibility and the Impossibility of Time Free Self-Stabilizing Failure Detection. http://hdl.handle.net/20.500.12708/32983
• Time Free Self-Stabilizing Local Failure Detection / Hutle, M., & Widder, J. (2004). Time Free Self-Stabilizing Local Failure Detection. http://hdl.handle.net/20.500.12708/32982
• Implementing Time Free Designs for Distributed Real-Time Systems (A Case Study) / Hermant, J.-F., & Widder, J. (2004). Implementing Time Free Designs for Distributed Real-Time Systems (A Case Study). http://hdl.handle.net/20.500.12708/32981

2003

• Booting clock synchronization in partially synchronous systems with hybrid node and link failures. / Widder, J., & Schmid, U. (2003). Booting clock synchronization in partially synchronous systems with hybrid node and link failures. http://hdl.handle.net/20.500.12708/32911
• Perfect failure detection with booting in partially synchronous systems / Widder, J., Le Lann, G., & Schmid, U. (2003). Perfect failure detection with booting in partially synchronous systems. http://hdl.handle.net/20.500.12708/32910

2002

• Switching on : how processes initialize for consistent broadcast / Widder, J. (2002). Switching on : how processes initialize for consistent broadcast [Diploma Thesis]. reposiTUm. https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-77756

• FIT-IT Embedded Systems Dissertationsstipendium "Distributed Computing in the Presence of Bounded Asynchrony"
  2004 / Austria

Soon, this page will include additional information such as reference projects, activities as journal reviewer and editor, memberships in councils and committees, and other research activities.

Until then, please visit Josef Widder’s research profile in TISS .