2019W

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

• LogiCs-Scholarships
  2017 – 2021 / LCS
• Bit-level Accurate Reasoning and Interpolation
  2016 – 2020 / Microsoft Research Limited
• Tools for Concurrent and distributed Systems
  2011 – 2019 / Austrian Science Fund (FWF)

2018

• Computer Aided Verification 2018 - Part II / H. Chockler, G. Weissenbacher / Springer, 2018, ISBN: 978-3-319-96141-5
• Computer Aided Verification 2018 - Part I / H. Chockler, G. Weissenbacher / Springer, 2018, ISBN: 978-3-319-96144-6
• Randomized testing of distributed systems with probabilistic guarantees / B. Kulahcioglu Ozkan, R. Majumdar, F. Niksic, M. Tabaei Befrouei, G. Weissenbacher / Proceedings of the ACM on Programming Languages, 2 (2018), OOPSLA
• Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms / T. Pani, G. Weissenbacher, F. Zuleger / Talk: International Conference on Formal Methods in Computer-Aided Design (FMCAD), Austin, TX; 2018-10-30 - 2018-11-02; in: "Formal Methods in Computer-Aided Design", FMCAD Inc., (2018), ISBN: 978-0-9835678-8-2; 1 - 9
• A Separation Logic with Data: Small Models and Automation / J. Katelaan, D. Jovanovic, G. Weissenbacher / Talk: 9th International Joint Conference on Automated Reasoning (IJCAR) 2018, Oxford; 2018-08-14 - 2018-08-17; in: "Automated Reasoning", LNCS, 10900 (2018), ISBN: 978-3-319-94204-9; 455 - 471

2017

• Interpolation-based Model Checking and IC3 / G. Weissenbacher / Keynote Lecture: Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science, Telč, Czech Republic (invited); 2017-10-13 - 2017-10-15
• FMCAD'17: Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design / D. Stewart, G. Weissenbacher / FMCAD Inc., Austin, TX, 2017, ISBN: 978-0-9835678-7-5; 241 pages
• Preface of the Special Issue in Memoriam Helmut Veith / G. Gottlob, T. Henzinger, G. Weissenbacher / Formal Methods in System Design, 51 (2017), 2; 267 - 269
• Model-based, mutation-driven test case generation via heuristic-guided branching search / A. Fellner, W. Krenn, R. Schlick, T. Tarrach, G. Weissenbacher / Talk: MEMOCODE 2017: the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, Wien; 2017-09-29 - 2017-10-02; in: "Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2017, Vienna, Austria, September 29 - October 02, 2017", ACM, (2017), ISBN: 978-1-4503-5093-8; 56 - 66
• Dynamic Reductions for Model Checking Concurrent Software / H. Günther, A. Laarman, A. Sokolova, G. Weissenbacher / Talk: Verification, Model Checking, and Abstract Interpretation (VMCAI), Paris; 2017-01-15 - 2017-01-17; in: "Verification, Model Checking, and Abstract Interpretation", Springer, Lecture Notes in Computer Science 10145 (2017), 246 - 265

2016

• Interpolation algorithms and their applications in model checking / G. Weissenbacher / Talk: Automata, Logic and Games, Singapore (invited); 2016-08-29 - 2016-09-02
• Abstraction and mining of traces to explain concurrency bugs / M. Tabaei Befrouei, C. Wang, G. Weissenbacher / Formal Methods in System Design, 49 (2016), 1; 1 - 32
• Labelled Interpolation Systems for Hyper-Resolution, Clausal, and Local Proofs / M. Schlaipfer, G. Weissenbacher / Journal of Automated Reasoning, 57 (2016), 1; 3 - 36
• Logical Methods in Automated Hardware and Software Verification / Habilitation Thesis by G. Weissenbacher / TU Wien/Fakultät für Informatik, 2016
• Error Invariants for Concurrent Traces / A. Holzer, D. Schwartz-Narbonne, M. Tabaei Befrouei, G. Weissenbacher, T. Wies / Talk: International Symposium on Formal Methods, Cyprus; 2016-11-07 - 2016-11-11; in: "Formal Methods", Lecture Notes in Computer Science/Springer, 9995 (2016), ISBN: 978-3-319-48988-9; 370 - 387

2015

• Under-approximating loops in C programs for fast counterexample detection / M. Lewis, D. Kroening, G. Weissenbacher / Formal Methods in System Design, 47 (2015), 1; 75 - 92
• Boolean Satisfiability Solvers and Their Applications in Model Checking / Y. Vizel, G. Weissenbacher, S. Malik / Proceedings of the IEEE (invited), 103 (2015), 11; 2021 - 2035
• Explaining Heisenbugs / G. Weissenbacher / Keynote Lecture: RV 2015, the 6th International Conference on Runtime Verification, Vienna (invited); 2015-09-22 - 2015-09-25; in: "Runtime Verification", E. Bartocci, R. Majumdar (ed.); Lecture Notes in Computer Science/Springer, 7408 (2015), ISBN: 978-3-319-23819-7; XV
• Proving Safety with Trace Automata and Bounded Model Checking / M. Lewis, D. Kroening, G. Weissenbacher / Talk: International Symposium on Formal Methods, Oslo, Norway; 2015-06-22 - 2015-06-25; in: "Formal Methods", Lecture Notes in Computer Science/Springer, 9109 (2015), ISBN: 978-3-319-19248-2; 325 - 341

2014

• Silicon fault diagnosis using sequence interpolation with backbones / C. Zhu, G. Weissenbacher, S. Malik / Talk: The IEEE/ACM International Conference on Computer-Aided Design (ICCAD), San Jose, CA, USA; 2014-11-03 - 2014-11-06; in: "ICCAD", IEEE Press Piscataway, NJ, USA, (2014), ISBN: 978-1-4799-6277-8; 348 - 355
• Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR) / J. Birgmeier, A. Bradley, G. Weissenbacher / Talk: International Conference on Computer Aided Verification (CAV), Wien; 2014-07-18 - 2014-07-22; in: "CAV", Springer / LNCS, 8559 (2014), ISBN: 978-3-319-08866-2; 829 - 846
• Reduction of Resolution Refutations and Interpolants via Subsumption / R. Bloem, S. Malik, M. Schlaipfer, G. Weissenbacher / Talk: Haifa Verification Conference (HVC), Haifa, Isral; 2014-11-18 - 2014-11-20; in: "Haifa Verification Conference (HVC)", Springer / LNCS, 8855 (2014), ISBN: 978-3-319-13337-9; 188 - 203
• Incremental bounded software model checking / H. Günther, G. Weissenbacher / Talk: International SPIN Symposium on Model Checking of Software (SPIN), San Jose, CA, USA; 2014-07-21 - 2014-07-23; in: "SPIN", ACM New York, NY, USA, (2014), ISBN: 978-1-4503-2452-6; 40 - 47
• Abstraction and Mining of Traces to Explain Concurrency Bugs / M. Tabaei Befrouei, C. Wang, G. Weissenbacher / Talk: nternational Conference on Runtime Verification, Toronto, Kanada; 2014-09-22 - 2014-09-25; in: "Runtime Verification", Springer / LNCS, 8734 (2014), ISBN: 978-3-319-11163-6; 162 - 177

2013

• Advanced SAT Techniques for Abstract Argumentation / J. P. Wallner, G. Weissenbacher, S. Woltran / Talk: International Workshop on Computational Logic in Multi-Agent Systems (CLIMA), Corunna, Spanien; 2013-09-16 - 2013-09-18; in: "CLIMA", Springer / LNCS, 8143 (2013), ISBN: 978-3-642-40623-2; 138 - 154
• Under-Approximating Loops in C Programs for Fast Counterexample Detection / D. Kroening, M. Lewis, G. Weissenbacher / Talk: International Conference on Computer Aided Verification (CAV), Sankt Petersburg, Russland; 2013-07-13 - 2013-07-19; in: "CAV", Springer / LNCS, 8044 (2013), ISBN: 978-3-642-39798-1; 381 - 396

2012

• Labelled Interpolation Systems / G. Weissenbacher / Talk: Dagstuhl Seminar 12461: Games and Decisions for Rigorous Systems Engineering, Dagstuhl, Deutschland (invited); 2012-11-11 - 2012-11-16
• Coverage-based Trace Signal Selection for Fault Localisation in Post-Silicon Validation / Z. Charlie Shucheng, G. Weissenbacher, S. Malik / Talk: Haifa Verification Conference (HVC), Haifa, Isral; 2012-11-06 - 2012-11-08; in: "Haifa Verification Conference (HVC)", Lecture Notes in Computer Science. Springer Verlag., 7857 (2012), ISBN: 978-3-642-39610-6; 132 - 147
• Parallel Assertions for Architectures with Weak Memory Models / D. Schwartz-Narbonne, G. Weissenbacher, S. Malik / Talk: Automated Technology for Verification and Analysis (ATVA), Thiruvananthapuram, India; 2012-10-03 - 2012-10-06; in: "Automated Technology for Verification and Analysis", Lecture Notes in Computer Science. Springer Verlag., 7561 (2012), ISBN: 978-3-642-33385-9; 254 - 268
• Interpolant Strength Revisited / G. Weissenbacher / Talk: International Conference on Theory and Applications of Satisfiability Testing (SAT), Trient, Italien; 2012-06-17 - 2012-06-20; in: "International Conference on Theory and Applications of Satisfiability Testing (SAT)", LNCS / Springer, 7317 (2012), 312 - 326

• Effective Error Explanation Techniques for Concurrent Software / PhD Thesis by M. Tabaei Befrouei / Supervisor, Reviewer: G. Weissenbacher, T. Eiter, R. Majumdar; Informationssysteme, 2016; oral examination: 2016-12-06
• Complexity Results and Algorithms for Argumentation - Dung's Frameworks and Beyond / PhD Thesis by J. P. Wallner / Supervisor, Reviewer: S. Woltran, G. Weissenbacher; Institute of Information Systems, 2014; oral examination: 2014-05-28
• Software Verification with IC3 via Abstraction and Interpolation / Master Thesis by J. Birgmeier / Supervisor: G. Weissenbacher, H. Veith; Fakultät für Informatik der Technischen Universität Wien, 2013