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)
• Proof Seeding for Software Verification
  2011 – 2015 / Vienna Science and Technology Fund (WWTF)
• Asynchronous Distributed Algorithms in the Theta-Model
  2004 – 2008 / Austrian Science Fund (FWF)
• 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 APIs for the new database have been released, everything will be up to date again.

2021

• Eliminating Message Counters in Synchronous Threshold Automata / I. Stoilkovska, I. Konnov, J. Widder, F. Zuleger / Talk: 22nd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), Copenhagen, Denmark; 2021-01-17 - 2021-01-19; in: "Proceedings of the 22nd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)", Springer LNCS, 12597 (2021), 196 - 218

2020

• Eliminating Message Counters in Threshold Automata / I. Stoilkovska, I. Konnov, J. Widder, F. Zuleger / in: "Automated Technology for Verification and Analysis - 18th Symposium, 2020, Hanoi, Vietnam", 12302; Springer LNCS, 2020, 196 - 212

2019

• Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking / I. Stoilkovska, I. Konnov, J. Widder, F. Zuleger / in: "International Conference on Tools and Algorithms for the Construction and Analysis of Systems", Springer, 2019, 357 - 374
• Verification of Randomized Consensus Algorithms Under Round-Rigid Adversaries / N. Bertrand, I. Konnov, M. Lazić, J. Widder / in: "30th International Conference on Concurrency Theory", Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, 2019, 33:1 - 33:15
• Communication-Closed Asynchronous Protocols / A. Damian, C. Dragoi, A. Militaru, J. Widder / in: "International Conference on Computer Aided Verification", Springer, 2019, 344 - 363

2018

• ByMC: Byzantine Model Checker / I. Konnov, J. Widder / Talk: International Symposium on Leveraging Applications of Formal Methods (ISoLA), Limasol, Zypern; 2018-11-05 - 2018-11-09; in: "ISOLA", Lecture Notes in Computer Science. Springer Verlag., 11246 (2018), ISBN: 978-3-642-34025-3; 327 - 342
• Reachability in Parameterized Systems: All Flavors of Threshold Automata / J. Kukovec, I. Konnov, J. Widder / Talk: International Conference on Concurrency Theory (CONCUR), Bejing, China; 2018-09-04 - 2018-09-07; in: "29th International Conference on Concurrency Theory (CONCUR 2018)", Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing, 118 (2018), ISBN: 978-3-95977-087-3; 19:1 - 19:17
• Communication-Closed Layers as Paradigm for Distributed Systems: A Manifesto / C. Dragoi, M. Lazić, J. Widder / Talk: Sinteza 2018 International Scientific Conference on Information Technology and Data Related Research, Belgrad, Serbien (invited); 2018-04-20; in: "Sinteza 2018 International Scientific Conference on Information Technology and Data Related Research", Singidunum University, 15 (2018), 131 - 138
• Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction / B. Aminof, I. Stoilkovska, S. Rubin, J. Widder, F. Zuleger / Talk: International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), Los Angeles; 2018-01-07 - 2018-01-09; in: "Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings", LNCS, 10747 (2018), ISBN: 978-3-319-73720-1; 1 - 24
• Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction / B. Aminof, S. Rubin, I. Stoilkovska, J. Widder, F. Zuleger / Talk: Verification, Model Checking, and Abstract Interpretation (VMCAI), Los Angeles; 2018-01-07 - 2018-01-09; in: "VMCAI", LNCS/Springer, 10747 (2018), 1 - 24
• Proceedings 32nd International Symposium on Distributed Computing / U. Schmid, J. Widder / Dagstuhl Publishing LIPICS, 2018, ISBN: 978-3-95977-092-7; 736 pages

2017

• Synthesis of Distributed Algorithms with Parameterized Threshold Guards / M. Lazić, I. Konnov, J. Widder, R. Bloem / Talk: International Conference On Principles Of Distributed Systems (OPODIS), Lissabon; 2017-12-18 - 2017-12-20; in: "OPODIS", LIPIcs-Leibniz International Proceedings in Informatics, (2017), 32:1 - 32:20
• A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms / I. Konnov, M. Lazić, H. Veith, J. Widder / Talk: 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), Paris, France; 2017-01-18 - 2017-01-20; in: "POPL", ACM, Paris (2017), ISBN: 978-1-4503-4660-3; 719 - 734
• Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms / I. Konnov, J. Widder, F. Spegni, L. Spalazzi / Talk: Verification, Model Checking, and Abstract Interpretation (VMCAI), Paris; 2017-01-15 - 2017-01-17; in: "VMCAI 2017: Verification, Model Checking, and Abstract Interpretation", Springer, LNCS/10145/Paris (2017), ISBN: 978-3-319-52233-3; 347 - 366
• On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability / I. Konnov, H. Veith, J. Widder / Information and Computation, 252 (2017), 95 - 109
• Para^2: Parameterized Path Reduction, Acceleration, and SMT for Reachability in Threshold-Guarded Distributed Algorithms / I. Konnov, M. Lazić, H. Veith, J. Widder / Formal Methods in System Design (invited), 51 (2017), 2; 270 - 307

2016

• Model Checking of Threshold-based Fault-Tolerant Distributed Algorithms / M. Lazić, I. Konnov, H. Veith, J. Widder / Talk: 7th Workshop on Program Semantics, Specification and Verification: Theory and Applications, St. Petersburg, Russia (invited); 2016-07-14 - 2016-07-15
• Parameterized Verification of Liveness of Distributed Algorithms / I. Konnov, M. Lazić, H. Veith, J. Widder / Talk: Workshop on Formal Reasoning in Distributed Algorithms (FRiDA), Marrakech, Marocco; 2016-05-17
• Decidability of Parameterized Verification / R. Bloem, S. Jacobs, A. Khalimov, I. Konnov, S. Rubin, H. Veith, J. Widder / ACM SIGACT News, 47 (2016), 2; 53 - 64

2015

• What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms / I. Konnov, H. Veith, J. Widder / Keynote Lecture: Perspectives of System Informatics: 10th International Andrei Ershov Informatics Conference, Kazan, Russland (invited); 2015-08-25 - 2015-08-27; in: "Perspectives of System Informatics: 10th International Andrei Ershov Informatics Conference, PSI 2015", LNCS / Springer, 9609 (2016), 6 - 21
• SMT and POR beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms / I. Konnov, H. Veith, J. Widder / Talk: International Conference on Computer Aided Verification (CAV), San Francisco, CA, USA; 2015-07-18 - 2015-07-24; in: "Computer Aided Verification", LNCS Springer, 9206 (2015), ISBN: 978-3-319-21689-8; 85 - 102
• Decidability of Parameterized Verification / R. Bloem, S. Jacobs, A. Khalimov, I. Konnov, S. Rubin, H. Veith, J. Widder / Morgan & Claypool Publishers, San Rafael, CA, USA, 2015, ISBN: 9781627057431; 170 pages
• Time Complexity of Link Reversal Routing / B. Charron-Bost, M Függer, L. Welch, J. Widder / ACM Transactions on Algorithms, 11 (2015), 3; 1 - 39

2014

• Approaching Verification and Validation Challenges in Smart Grids / T. Deutsch, J. Widder / Talk: Symposium Communications for Energy Systems, Wien; 2014-09-29 - 2014-10-01; in: "Tagungsband ComForEn 2014", Eigenverlag des Österreich isch en Verbandes für Elektrotec h nik, (2014), ISBN: 978-3-85133-083-0; 6 pages
• On the Completeness of Bounded Model Checking for Threshold-Based Distributed Algorithms: Reachability / I. Konnov, H. Veith, J. Widder / Talk: International Conference on Concurrency Theory (CONCUR), Rom, Italien; 2014-09-02 - 2014-09-05; in: "CONCUR", (2014), 125 - 140
• Solvability-Based Comparison of Failure Detectors / S. Sastry, J. Widder / Talk: International Symposium on Network Computing and Applications (NCA), Boston, MA, USA; 2014-08-21 - 2014-08-23; in: "NCA", IEEE Computer Society, (2014), ISBN: 978-1-4799-5392-9; 269 - 276
• A Logic-Based Framework for Verifying Consensus Algorithms / C. Dragoi, T. Henzinger, H. Veith, J. Widder, D. Zufferey / Talk: Verification, Model Checking, and Abstract Interpretation (VMCAI), San Diego; 2014-02-19 - 2014-02-21; in: "VMCAI", Springer / LNCS, 8318 (2014), ISBN: 978-3-642-54012-7; 161 - 181
• Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms / A. Gmeiner, I. Konnov, U. Schmid, H. Veith, J. Widder / in: "Formal Methods for Executable Software Models", Springer, 2014, (invited), ISBN: 978-3-319-07316-3, 122 - 171

2013

• Parameterized model checking of fault-tolerant distributed algorithms by abstraction / A. John, I. Konnov, U. Schmid, H. Veith, J. Widder / Talk: International Conference on Formal Methods in Computer-Aided Design (FMCAD), Portland, OR, USA; 2013-10-20 - 2013-10-23; in: "FMCAD", (2013), ISBN: 978-0-9835678-3-7; 201 - 209
• Brief announcement: parameterized model checking of fault-tolerant distributed algorithms by abstraction / A. John, I. Konnov, U. Schmid, H. Veith, J. Widder / Talk: ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing (PODC), Montreal, Kanada; 2013-07-22 - 2013-07-24; in: "PODC", ACM, (2013), ISBN: 978-1-4503-2065-8; 119 - 121
• Towards Modeling and Model Checking Fault-Tolerant Distributed Algorithms / A. John, I. Konnov, U. Schmid, H. Veith, J. Widder / Talk: International SPIN Symposium on Model Checking of Software (SPIN), Stony Brook, NY, USA; 2013-07-08 - 2013-07-09; in: "SPIN", LNCS, Springer, 7976 (2013), ISBN: 978-3-642-39175-0; 209 - 226
• Formal Verification of Distributed Algorithms (Dagstuhl Seminar 13141) / B. Charron-Bost, A. Rybalchenko, S. Merz, J. Widder / in series "Dagstuhl Reports", series editor: Schloss Dagstuhl; issued by: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik; Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, Dagstuhl, Deutschland, 2013, ISSN: 2192-5283, 16 pages
• Link Reversal Routing with Binary Link Labels: Work Complexity / B. Charron-Bost, A. Gaillard, L. Welch, J. Widder / SIAM JOURNAL ON COMPUTING, 42 (2013), 2; 634 - 661

2012

• Wait-Free Stabilizing Dining Using Regular Registers / S. Sastry, L. Welch, J. Widder / Talk: International Conference On Principles Of Distributed Systems (OPODIS), Rom; 2012-12-17 - 2012-12-20; in: "OPODIS", LNCS / Springer, 7702 (2012), ISBN: 978-3-642-35475-5; 284 - 299
• Parameterized Model Checking of Fault-tolerant Distributed Algorithms / A. John, I. Konnov, U. Schmid, H. Veith, J. Widder / Talk: Dagstuhl Seminar 12461: Games and Decisions for Rigorous Systems Engineering, Dagstuhl, Deutschland (invited); 2012-11-11 - 2012-11-16
• Who is afraid of Model Checking Distributed Algorithms? / A. John, I. Konnov, U. Schmid, H. Veith, J. Widder / Talk: PUMA/RISE Seminar, Goldegg; 2012-09-24 - 2012-09-28
• Efficient Checking of Link-Reversal-Based Concurrent Systems / M Függer, J. Widder / Talk: International Conference on Concurrency Theory (CONCUR), Newcaslte upon Tyne, UK; 2012-09-03 - 2012-09-08; in: "CONCUR 2012 - Concurrency Theory", Lecture Notes in Computer Science. Springer Verlag., 7454 (2012), ISBN: 978-3-642-32939-5; 486 - 499
• Who is afraid of Model Checking Distributed Algorithms? / I. Konnov, H. Veith, J. Widder / Talk: Workshop on Exploiting Concurrency Efficiently and Correctly, Berkeley, CA, USA; 2012-07-07 - 2012-07-08
• Counter Attack against Byzantine Generals / A. John, I. Konnov, U. Schmid, H. Veith, J. Widder / Talk: Alpine Verification Meeting, Passau, Bayern, Deutschland; 2012-05-21 - 2012-05-22
• Consensus in the presence of mortal Byzantine faulty processes / J. Widder, M. Biely, G. Gridling, B. Weiss, J. Blanquart / Distributed Computing, 24 (2012), 6; 299 - 321

2011

• On Efficient Checking of Link-reversal-based Concurrent Systems / M Függer, J. Widder / Talk: PUMA/RISE Seminar, Traunkirchen; 2011-10-03 - 2011-10-07

2010

• In search of lost time / B. Charron-Bost, M. Hutle, J. Widder / Information Processing Letters, 110 (2010), 21; 928 - 933

2009

• Routing without Ordering / B. Charron-Bost, A. Gaillard, L. Welch, J. Widder / Talk: SPAA 2009 (Parallelism in Algorithms and Architectures), Calgary, Alberta, Canada; 2009-08-11 - 2009-08-13; in: "Proceedings of the Twenty-First Annual Symposium on Parallelism in Algorithms and Architectures", ACM, (2009), ISBN: 978-1-60558-606-9; 145 - 153
• Link Reversal: How to Play Better to Work Less / B. Charron-Bost, L. Welch, J. Widder / Talk: ALGOSENSORS 2009 (5th International Workshop on Algorithmic Aspects of Wireless Sensor Networks), Rhodes, Greece; 2009-07-10 - 2009-07-11; in: "Algorithmic Aspects of Wireless Sensor Networks", Springer, 5304/2008 (2009), ISBN: 9783642054334; 88 - 110
• Optimal Message-Driven Implementations of Omega with Mute Processes / J. Widder, M. Biely / ACM Transactions on Autonomous and Adaptive Systems., 4 (2009), 1; ?
• The Theta-Model: achieving synchrony without clocks / J. Widder, U. Schmid / Distributed Computing, 22 (2009), 1; 29 - 47

2007

• Clock Synchronization in the Byzantine-Recovery Failure Model / E. Anceaume, C. Delporte-Gallet, H. Fauconnier, M. Hurfin, J. Widder / Talk: International Conference On Principles Of Distributed Systems (OPODIS), Guadeloupe; 2007-12-17 - 2007-12-20; in: "International Conference On Principles Of DIstributed System", (2007), 90 - 104
• Relating Stabilizing Timing Assumptions to Stabilizing Failure Detectors Regarding Solvability and Efficiency / M. Biely, M. Hutle, L. Penso, J. Widder / Talk: Ninth International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2007), Paris; 2007-11-14 - 2007-11-16; in: "stabilization", (2007)
• Tolerating Corrupted Communication / M. Biely, B. Charron-Bost, A. Gaillard, M. Hutle, A. Schiper, J. Widder / Talk: ACM Symposium on Principles of Distributed Computing, Portland; 2007-08-12 - 2007-08-15; in: "26th ACM Symposium on Principles of Distributed Computing (PODC'07)", (2007), 244 - 253
• Synchronous Consensus with Mortal Byzantines / J. Widder, G. Gridling, B. Weiss, J. Blanquart / Talk: IEEE Conference on Dependable Systems and Networks (DSN), Edinburgh; 2007-06-25 - 2007-06-28; in: "Proceedings of the 37th Annual IEEE/IFIP International Conference on Dependable Systems and Networks", (2007)
• Booting Clock Synchronization in Partially Synchronous Systems with Hybrid Process and Link Failures / J. Widder, U. Schmid / in: "Distributed Computing", Springer-Verlag, 2007, 115 - 140

2006

• Optimal Message-Driven Implementations of Omega with Mute Processes / M. Biely, J. Widder / Talk: 8th International Symposium on Stabilization, Safety, and Security of Distributed Systems, Dallas; 2006-11-17 - 2006-11-19; in: "Stabilization, Safety, and Security of Distributed Systems", (2006), 110 - 121
• An Efficient Test for a Transition Signalling based Up-/Down-Counter / M Függer, T. Handl, A. Steininger, J. Widder, C. Tögel / Poster: Austrochip, Wien; 2006-10-11; in: "Austrochip Mikroelektroniktagung", (2006), 55 - 62
• Synchronous Consensus with Mortal Byzantines / J. Widder, G. Gridling, B. Weiss, J. Blanquart / Talk: Dagstuhl Seminar 06371. From Security to Dependability, Dagstuhl (invited); 2006-09-10 - 2006-09-15
• Simulating Distributed Real-Time Systems / D. Albeseder, J. Widder / Poster: Junior Scientist Conference, Wien; 2006-04-19 - 2006-04-21; in: "Junior Scientist Conference 2006", (2006), 83 - 84

2005

• Implementing Reliable Distributed Real Time Systems with the Theta Model / J.-F. Hermant, J. Widder / Talk: International Conference on Principles of Distributed Systems, Pisa; 2005-12-12 - 2005-12-14; in: "9th International Conference on Principles of Distributed Systems", (2005), 259 - 271
• On the Possibility and the Impossibility of Message-Driven Self-Stabilizing Failure Detection / M. Hutle, J. Widder / Talk: Seventh International Symposium on Self Stabilizing Systems (SSS 2005), Barcelona, Spanien; 2005-10-26 - 2005-10-27; in: "Self Stabilizing Systems", (2005), 153 - 170
• Brief Announcement: On the Possibility and the Impossibility of Message-Driven Self-Stabilizing Failure Detection / M. Hutle, J. Widder / Talk: ACM Symposium on Principles of Distributed Computing, Las Vegas, Nevada; 2005-07-17 - 2005-07-20; in: "Proceedings of the 24th ACM Symposium on Principles of Distributed Computing", (2005), 208
• Failure Detection with Booting in Partially Synchronous Systems / J. Widder, G. Le Lann, U. Schmid / Talk: European Dependable Computing Conference, Budapest, Ungarn; 2005-04-20 - 2005-04-22; in: "Dependable Computing Conference - EDCC5", (2005), 20 - 37
• Self-Stabilizing Failure Detector Algorithms / M. Hutle, J. Widder / Talk: IASTED International Conference on Parallel and Distributed Computing Systems, Innsbruck, Austria; 2005-02-15 - 2005-02-17; in: "IASTED International Conference on Parallel and Distributed Computing and Networks", (2005), ISBN: 0-88986-468-3; 485 - 490

2004

• VLSI Design and the Theta-Model (Kurzvorstellungen aktueller Forschung) / J. Widder / Talk: Diskussionskreis Fehlertoleranz, Berlin; 2004-11-12
• Why, Where and How to Use the Theta-Model / J. Widder / Talk: Seminaire Reflecs in INRIA Rocquencourt, Frankreich, INRIA Rocquencourt, Frankreich (invited); 2004-03-10
• The Theta-Model, and how to Boot Clock Synchronization in it / J. Widder / Talk: Seminaire Reflecs in INRIA Rocquencourt, Frankreich, INRIA Rocquencourt, Frankreich (invited); 2004-02-10
• Distributed Computing in the Presence of Bounded Asynchrony / Doctoral Thesis by J. Widder / Supervisor, Reviewer: U. Schmid, M. Jazayeri; Institut für Technische Informatik / Embedded Computing Systems, 2004
• On the Possibility and the Impossibility of Time Free Self-Stabilizing Failure Detection / M. Hutle, J. Widder / Report for Research Report 34/2004, Technische Universität Wien, Institut für Technische Informatik, Treitlstraße 3, A-1040 Vienna, Austria; 2004
• Time Free Self-Stabilizing Local Failure Detection / M. Hutle, J. Widder / Report for Research Report 33/2004, Technische Universität Wien, Institut für Technische Informatik, Treitlstraße 3, A-1040 Vienna, Austria; 2004
• Implementing Time Free Designs for Distributed Real-Time Systems (A Case Study) / J.-F. Hermant, J. Widder / Report for Research Report 23/2004, Technische Universität Wien, Institut für Technische Informatik, Treitlstraße 3, A-1040 Vienna, Austria (Joint research report with INRIA Rocquencourt, France); 2004

2003

• Booting clock synchronization in partially synchronous systems. / J. Widder / Talk: International Conference on Distributed Computing Systems, Sorrento, Italy; 2003-10-01 - 2003-10-03; in: "Proceedings of the 17th International Symposium on Distributed Computing ", (2003), 121 - 135
• Perfect failure detection with booting in partially synchronous systems / J. Widder, G. Le Lann, U. Schmid / Report for Technical Report 183/1-131, Department of Automation, Technische Universität Wien; 2003
• Booting clock synchronization in partially synchronous systems with hybrid node and link failures. / J. Widder, U. Schmid / Report for Technical Report 183/1-126, Department of Automation, Technische Universität Wien; 2003

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