2021W

• Bachelor Thesis / 184.695 / PR
• Doctoral & Master Students Seminar / 181.224 / SE
• Introduction to Logical Methods in Computer Science / 184.766 / VO
• Project in Computer Science 1 / 184.692 / PR
• Project in Computer Science 2 / 184.693 / PR
• Research Seminar LogiCS / 184.767 / SE
• Scientific Research and Writing / 193.052 / SE
• Seminar Formal Methods / 181.221 / SE
• Software Model Checking / 192.106 / VU

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

2021

• Bounded Model Checking of Speculative Non-Interference / E. Pescosta, G. Weissenbacher, F. Zuleger / Talk: 2021 IEEE/ACM International Conference On Computer Aided Design (ICCAD), München, Deutschland; 2021-11-01 - 2021-11-04; in: "2021 IEEE/ACM International Conference On Computer Aided Design (ICCAD)", IEEE, (2021), ISBN: 978-1-6654-4507-8; 1 - 9
• Model Checking AUTOSAR Components with CBMC / T. Durand, K. Fazekas, G. Weissenbacher, J. Zwirchmayr / Talk: Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design - FMCAD 2021, New Haven, Connecticut, USA; 2021-10-19 - 2021-10-22; in: "Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design - FMCAD 2021", R. Piskac, M. Whalen (ed.); TU Wien Academic Press, 2 (2021), ISBN: 978-3-85448-046-4; 96 - 101
• Rely-guarantee bound analysis of parameterized concurrent shared-memory programs / T. Pani, G. Weissenbacher, F. Zuleger / Formal Methods in System Design, 57 (2021), 2; 270 - 302
• Mutation testing with hyperproperties / A. Fellner, M. Tabaei Befrouei, G. Weissenbacher / Journal of Software and Systems Modeling (online-edition), 20 (2021), 2; 405 - 427
• Preface of the special issue on the conference on computer-aided verification 2018 / H. Chockler, G. Weissenbacher / Formal Methods in System Design, 57 (2021), 1; 1 - 2

2020

• Thread-modular Counter Abstraction for Parameterized Program Safety / T. Pani, G. Weissenbacher, F. Zuleger / Talk: International Conference on Formal Methods in Computer-Aided Design (FMCAD), Haifa, Israel; 2020-09-22 - 2020-09-24; in: "Formal Methods in Computer-Aided Design", TU Wien Academic Press / IEEE, 1 (2020), ISBN: 978-3-85448-042-6; 67 - 76
• Multi-linear Strategy Extraction for QBF Expansion Proofs via Local Soundness / M. Schlaipfer, F. Slivovsky, G. Weissenbacher, F. Zuleger / Talk: International Conference on the Theory and Applications of Satisfiability Testing, Alghero, Italien; 2020-07-03 - 2020-07-10; in: "SAT 2020: Theory and Applications of Satisfiability Testing - SAT 2020", LNCS, 12178 (2020), ISBN: 978-3-030-51824-0; 429 - 446
• RAT Elimination / A. Rebola Pardo, G. Weissenbacher / Talk: International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Alicante, Spain; 2020-05-22 - 2020-05-27; in: "Logic for Programming, Artificial Intelligence and Reasoning", L. Kovacs, E. Albert (ed.); EasyChair, 73 (2020), 423 - 448
• Language Inclusion for Finite Prime Event Structures / A. Fellner, T. Tarrach, G. Weissenbacher / Talk: International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), New Orleans, LA, USA; 2020-01-16 - 2020-01-21; in: "Verification, Model Checking, and Abstract Interpretation", Springer, LNCS 11990 (2020), ISBN: 978-3-030-39321-2; 314 - 336
• Extracting safe thread schedules from incomplete model checking results / P. Metzler, N. Suri, G. Weissenbacher / International Journal on Software Tools for Technology Transfer, 22 (2020), 5; 565 - 581
• Preface of the Special Issue on the Conference on Formal Methods in Computer-Aided Design 2017 / D. Stewart, G. Weissenbacher / Formal Methods in System Design, 56 (2020), 1-3; 1

2019

• Mutation Testing with Hyperproperties / A. Fellner, M. Tabaei Befrouei, G. Weissenbacher / Talk: 17th International Conference on Software Engineering and Formal Methods, Oslo, Norway; 2019-09-18 - 2019-09-20; in: "Proc. of SEFM 2019: the 17th International Conference on Software Engineering and Formal Methods", 11724 (2019), 203 - 221
• Model-Based Diagnosis with Multiple Observations / A. Ignatiev, A. Morgado, J. Marques-Silva, G. Weissenbacher / Talk: IJCAI 2019 - 28th International Joint Conference on Artificial Intelligence, Macao, China; 2019-08-10 - 2019-08-16; in: "International Joint Conference on Artificial Intelligence", (2019), ISBN: 978-0-9992411-4-1; 1108 - 1115
• Extracting Safe Thread Schedules from Incomplete Model Checking Results / P. Metzler, N. Suri, G. Weissenbacher / Talk: International SPIN Symposium on Model Checking of Software (SPIN), Beijing, China; 2019-07-15 - 2019-07-16; in: "Model Checking Software", LNCS, Springer, 11636 (2019), ISBN: 978-3-030-30922-0; 153 - 171
• Model-based, Mutation-driven Test-case Generation Via Heuristic-guided Branching Search / A. Fellner, W. Krenn, R. Schlick, T. Tarrach, G. Weissenbacher / ACM Transactions on Embedded Computing Systems, 18 (2019), 1

2018

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

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

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

2015

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

2014

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

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

• Static Analysis of Low-Level Code / Doctoral Thesis by I. Grishchenko / Supervisor, Reviewer: M. Maffei, G. Weissenbacher, A. Sabelfeld, K. Bhargavan; Institut of Logic and Computation, Security and Privacy, 2021; oral examination: 2021-01-25
• SpecBMC : bounded model checker for speculative non-interference / Master Thesis by E. Pescosta / Supervisor: G. Weissenbacher, F. Zuleger; Logic and Computation, 2020
• Verifying automotive software components using C model checkers / Master Thesis by T. Durand / Supervisor: G. Weissenbacher, W. Steiner; Logic and Computation, 2020
• Abstraction for Reasoning about Agent Behavior with Answer Set Programming / Doctoral Thesis by Z. G. Saribatur / Supervisor, Reviewer: T. Eiter, G. Weissenbacher; Institut für Logic and Computation, 2019; oral examination: 2019-12-17
• Effective Error Explanation Techniques for Concurrent Software / Doctoral 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 / Doctoral 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