TU Wien Informatics

Overview Professors Scientific Staff Administrative Staff Student Staff External Lecturers By Responsibilities By Committee By Name
Related
Guest Professors Honoraries Alumni (LinkedIn) #5qw

Josef Widder

Privatdoz. Dipl.-Ing. Dr.techn.

Research Focus

  • Computer Engineering: 50%
  • Logic and Computation: 50%

Research Areas

  • Proof-based System Engineering, Fault-tolerant systems, Formal verification, Dependable Systems, model checking, Real-time systems, Distributed Computing
Josef Widder

Role

Contact

2025S

 

2022

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 VMCAI 2021: Verification, Model Checking, and Abstract Interpretation (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
    Download: PDF (408 KB)
  • Tutorial: Parameterized Verification with Byzantine Model Checker / Konnov, I., Lazic, M., Stoilkovska, I., & Widder, J. (2020). Tutorial: Parameterized Verification with Byzantine Model Checker. In Formal Techniques for Distributed Objects, Components, and Systems. 40th IFIP WG 6.1 International Conference, FORTE 2020, Held as Part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Valletta, Malta, June 15–19, 2020, Proceedings (pp. 189–207). Springer. https://doi.org/10.34726/422
    Download: PDF (391 KB)

2019

  • 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 W. Fokkink & R. van Glabbeek (Eds.), 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
  • 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
  • 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

  • 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, Serbia. Singidunum University. https://doi.org/10.15308/sinteza-2018-131-138
  • 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 S. Schewe & L. Zhang (Eds.), 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 T. Margaria & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems. ISoLA 2018, Proceedings, Part III (pp. 327–342). Springer. https://doi.org/10.1007/978-3-030-03424-5_22
  • 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 I. Dillig & J. Palsberg (Eds.), Verification, Model Checking, and Abstract Interpretation : 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings. Cham. https://doi.org/10.1007/978-3-319-73721-8_1
    Download: PDF (538 KB)
  • 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

2017

2016

  • What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms / Konnov, I., Veith, H., & Widder, J. (2016). What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms. In 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 (pp. 6–21). Springer. https://doi.org/10.1007/978-3-319-41579-6_2
    Download: PDF (346 KB)
  • 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

2014

  • 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 Formal Methods for Executable Software Models (pp. 122–171). Springer. https://doi.org/10.1007/978-3-319-07317-0_4
  • 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 Verification, Model Checking, and Abstract Interpretation 15th International Conference, VMCAI 2014, San Diego, CA, USA, January 19-21, 2014, Proceedings (pp. 161–181). Springer / LNCS. https://doi.org/10.1007/978-3-642-54013-4_10
  • 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
  • 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

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

  • Efficient Checking of Link-Reversal-Based Concurrent Systems / Függer, M., & Widder, J. (2012). Efficient Checking of Link-Reversal-Based Concurrent Systems. In CONCUR 2012- Concurrency Theory 23rd International Conference, CONCUR 2012, Newcastle upon Tyne, September 4-7, 2012. Proceedings (pp. 486–499). Lecture Notes in Computer Science. Springer Verlag. https://doi.org/10.1007/978-3-642-32940-1_34
  • Wait-Free Stabilizing Dining Using Regular Registers / Sastry, S., Welch, J. L., & Widder, J. (2012). Wait-Free Stabilizing Dining Using Regular Registers. In Principles of Distributed Systems 16th International Conference, OPODIS 2012, Rome, Italy, December 18-20, 2012, Proceedings (pp. 284–299). LNCS / Springer. https://doi.org/10.1007/978-3-642-35476-2_20
  • 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

2011

  • Brief announcement / Charron-Bost, B., Fuegger, M., Welch, J. L., & Widder, J. (2011). Brief announcement. In Proceedings of the 23rd ACM symposium on Parallelism in algorithms and architectures - SPAA ’11. SPAA ’11, San Jose, California, USA, Non-EU. ACM. https://doi.org/10.1145/1989493.1989510
  • Partial is Full / Charron-Bost, B., Függer, M., Welch, J. L., & Widder, J. (2011). Partial is Full. In Structural Information and Communication Complexity (pp. 113–124). Springer Berlin / Heidelberg. https://doi.org/10.1007/978-3-642-22212-2_11
  • Full Reversal Routing as a Linear Dynamical System / Charron-Bost, B., Függer, M., Welch, J. L., & Widder, J. (2011). Full Reversal Routing as a Linear Dynamical System. In Structural Information and Communication Complexity (pp. 101–112). Springer Berlin / Heidelberg. https://doi.org/10.1007/978-3-642-22212-2_10
  • 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

  • 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
  • Optimal Message-Driven Implementations of Omega with Mute Processes / Biely, M., & Widder, J. (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.1462191
  • 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

  • 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
  • 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

2006

2005

2004

2003

2002

 

  • 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 .