Georg Weissenbacher
Univ.Prof. Dipl.-Ing. / D.Phil.
Research Focus
- Computer Engineering: 30%
- Logic and Computation: 70%
About
Automated Software Verification
Role
-
Full Professor
Formal Methods in Systems Engineering, E192-04
Courses
2022W
- Bachelor Thesis / 184.695 / PR
- Computer Aided Verification / 181.145 / VU
- Computer-Aided Verification / 181.144 / UE
- 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
2023S
- Bachelor Thesis / 184.695 / PR
- Doctoral & Master Students Seminar / 181.224 / SE
- Introduction to Logical Methods in Computer Science / 184.766 / VO
- Program and System Verification / 184.741 / VU
- 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
Projects
-
AutoTest
2020 – 2021 / Vienna Science and Technology Fund (WWTF) -
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)
Publications
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
- 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. Pagel, 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
Supervisions
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.
- 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