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

Georg Weissenbacher

Univ.Prof. Dipl.-Ing. / D.Phil.

Research Focus

  • Computer Engineering: 30%
  • Logic and Computation: 70%
Georg Weissenbacher

About

Automated Software Verification

Roles

Contact

2024W

2025S

 

2024

2023

  • A Formalization of Heisenbugs and Their Causes / Sallinger, S., Weissenbacher, G., & Zuleger, F. (2023). A Formalization of Heisenbugs and Their Causes. In C. Ferreira & T. A. C. Willemse (Eds.), Software Engineering and Formal Methods : 21st International Conference, SEFM 2023, Eindhoven, The Netherlands, November 6-10, 2023, Proceedings (pp. 282–300). Springer. https://doi.org/10.34726/5381
    Download: Preprint for self-archivation (552 KB)
    Project: ARTIST (2021–2026)

2021

  • Model Checking AUTOSAR Components with CBMC / Durand, T., Fazekas, K., Weissenbacher, G., & Zwirchmayr, J. (2021). Model Checking AUTOSAR Components with CBMC. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 96–101). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_18
    Download: PDF (206 KB)
  • Bounded Model Checking of Speculative Non-Interference / Pescosta, E., Weissenbacher, G., & Zuleger, F. (2021). Bounded Model Checking of Speculative Non-Interference. In 2021 IEEE/ACM International Conference On Computer Aided Design (ICCAD). 2021 IEEE/ACM International Conference On Computer Aided Design (ICCAD), München, Germany. IEEE. https://doi.org/10.1109/iccad51958.2021.9643462
  • Preface of the special issue on the conference on computer-aided verification 2018 / Chockler, H., & Weissenbacher, G. (2021). Preface of the special issue on the conference on computer-aided verification 2018. Formal Methods in System Design. https://doi.org/10.1007/s10703-021-00365-5
  • Mutation testing with hyperproperties / Fellner, A., Tabaei Befrouei, M., & Weissenbacher, G. (2021). Mutation testing with hyperproperties. Software and Systems Modeling, 20(2), 405–427. https://doi.org/10.1007/s10270-020-00850-1
  • Rely-guarantee bound analysis of parameterized concurrent shared-memory programs / Pani, T., Weissenbacher, G., & Zuleger, F. (2021). Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. Formal Methods in System Design, 57(2), 270–302. https://doi.org/10.1007/s10703-021-00370-8

2020

  • Thread-modular Counter Abstraction for Parameterized Program Safety / Pani, T., Weissenbacher, G., & Zuleger, F. (2020). Thread-modular Counter Abstraction for Parameterized Program Safety. In A. Ivrii & O. Strichman (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 (pp. 67–76). TU Wien Academic Press. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_13
    Download: Published version (434 KB)
  • Language Inclusion for Finite Prime Event Structures / Fellner, A., Tarrach, T., & Weissenbacher, G. (2020). Language Inclusion for Finite Prime Event Structures. In Verification, Model Checking, and Abstract Interpretation 21st International Conference, VMCAI 2020, New Orleans, LA, USA, January 16–21, 2020, Proceedings (pp. 314–336). Springer. https://doi.org/10.1007/978-3-030-39322-9_15
  • Thread-modular Counter Abstraction for Parameterized Program Safety / Pani, T., Weissenbacher, G., & Zuleger, F. (2020). Thread-modular Counter Abstraction for Parameterized Program Safety. In Formal Methods in Computer-Aided Design (pp. 67–76). TU Wien Academic Press / IEEE. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_13
  • Multi-linear Strategy Extraction for QBF Expansion Proofs via Local Soundness / Schlaipfer, M., Slivovsky, F., Weissenbacher, G., & Zuleger, F. (2020). Multi-linear Strategy Extraction for QBF Expansion Proofs via Local Soundness. In Theory and Applications of Satisfiability Testing – SAT 2020 (pp. 429–446). LNCS. https://doi.org/10.1007/978-3-030-51825-7_30
  • RAT Elimination / Rebola Pardo, A., & Weissenbacher, G. (2020). RAT Elimination. In L. Kovacs & E. Albert (Eds.), EPiC Series in Computing. EasyChair. https://doi.org/10.29007/fccb
  • Preface of the Special Issue on the Conference on Formal Methods in Computer-Aided Design 2017 / Stewart, D., & Weissenbacher, G. (2020). Preface of the Special Issue on the Conference on Formal Methods in Computer-Aided Design 2017. Formal Methods in System Design, 57(3), 303–304. https://doi.org/10.1007/s10703-020-00357-x
  • Extracting safe thread schedules from incomplete model checking results / Metzler, P., Suri, N., & Weissenbacher, G. (2020). Extracting safe thread schedules from incomplete model checking results. International Journal on Software Tools for Technology Transfer, 22(5), 565–581. https://doi.org/10.1007/s10009-020-00575-y

2019

  • Extracting Safe Thread Schedules from Incomplete Model Checking Results / Metzler, P., Suri, N., & Weissenbacher, G. (2019). Extracting Safe Thread Schedules from Incomplete Model Checking Results. In Model Checking Software (pp. 153–171). LNCS, Springer. https://doi.org/10.1007/978-3-030-30923-7_9
  • Model-Based Diagnosis with Multiple Observations / Ignatiev, A., Morgado, A., Marques-Silva, J., & Weissenbacher, G. (2019). Model-Based Diagnosis with Multiple Observations. In Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence. IJCAI 2019 - 28th International Joint Conference on Artificial Intelligence, Macao, Macao. https://doi.org/10.24963/ijcai.2019/155
  • Mutation Testing with Hyperproperties / Fellner, A., Befrouei, M. T., & Weissenbacher, G. (2019). Mutation Testing with Hyperproperties. In Software Engineering and Formal Methods (pp. 203–221). https://doi.org/10.1007/978-3-030-30446-1_11
  • Model-based, Mutation-driven Test-case Generation Via Heuristic-guided Branching Search / Fellner, A., Krenn, W., Schlick, R., Tarrach, T., & Weissenbacher, G. (2019). Model-based, Mutation-driven Test-case Generation Via Heuristic-guided Branching Search. ACM Transactions on Embedded Computing Systems, 18(1), 1–28. https://doi.org/10.1145/3289256

2018

  • Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms / Pani, T., Weissenbacher, G., & Zuleger, F. (2018). Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms. In 2018 Formal Methods in Computer Aided Design (FMCAD). International Conference on Formal Methods in Computer-Aided Design (FMCAD), Portland, United States of America (the). FMCAD Inc. https://doi.org/10.23919/fmcad.2018.8603020
  • A Separation Logic with Data: Small Models and Automation / Pagel, J., Jovanovic, D., & Weissenbacher, G. (2018). A Separation Logic with Data: Small Models and Automation. In Automated Reasoning (pp. 455–471). LNCS. https://doi.org/10.1007/978-3-319-94205-6_30
  • A Counting Semantics for Monitoring LTL Specifications over Finite Traces / Bartocci, E., Bloem, R., Nickovic, D., & Roeck, F. (2018). A Counting Semantics for Monitoring LTL Specifications over Finite Traces. In H. Chockler & G. Weissenbacher (Eds.), Computer Aided Verification: 30th International Conference, CAV 2018 (pp. 547–564). Springer. https://doi.org/10.1007/978-3-319-96145-3_29
  • Reachable Set Over-Approximation for Nonlinear Systems Using Piecewise Barrier Tubes / Kong, H., Bartocci, E., & Henzinger, T. A. (2018). Reachable Set Over-Approximation for Nonlinear Systems Using Piecewise Barrier Tubes. In H. Chockler & G. Weissenbacher (Eds.), Computer Aided Verification: 30th International Conference, CAV 2018 (pp. 449–467). Springer. https://doi.org/10.1007/978-3-319-96145-3_24
  • Randomized testing of distributed systems with probabilistic guarantees / Ozkan, B. K., Majumdar, R., Niksic, F., Befrouei, M. T., & Weissenbacher, G. (2018). Randomized testing of distributed systems with probabilistic guarantees. Proceedings of the ACM on Programming Languages, 2(OOPSLA), 1–28. https://doi.org/10.1145/3276530
  • Foundations and Tools for the Static Analysis of Ethereum Smart Contracts / Gishchenko, I., Maffei, M., & Schneidewind, C. (2018). Foundations and Tools for the Static Analysis of Ethereum Smart Contracts. In G. Weissenbacher & H. Chockler (Eds.), Computer Aided Verification (pp. 51–78). Springer Open. https://doi.org/10.1007/978-3-319-96145-3_4
  • Computer Aided Verification / Computer Aided Verification. (2018). In H. Chockler & G. Weissenbacher (Eds.), Lecture Notes in Computer Science. Springer. https://doi.org/10.1007/978-3-319-96142-2
  • Computer Aided Verification / Computer Aided Verification. (2018). In H. Chockler & G. Weissenbacher (Eds.), Lecture Notes in Computer Science. Springer. https://doi.org/10.1007/978-3-319-96145-3

2017

  • Dynamic Reductions for Model Checking Concurrent Software / Günther, H., Laarman, A., Sokolova, A., & Weissenbacher, G. (2017). Dynamic Reductions for Model Checking Concurrent Software. In Verification, Model Checking, and Abstract Interpretation 18th International Conference, VMCAI 2017, Paris, France, January 15–17, 2017, Proceedings (pp. 246–265). Springer. https://doi.org/10.1007/978-3-319-52234-0_14
  • Model-based, mutation-driven test case generation via heuristic-guided branching search / Fellner, A., Krenn, W., Schlick, R., Tarrach, T., & Weissenbacher, G. (2017). Model-based, mutation-driven test case generation via heuristic-guided branching search. In Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design. MEMOCODE 2017: the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, Wien, Austria. ACM. https://doi.org/10.1145/3127041.3127049
  • Interpolation-based Model Checking and IC3 / Weissenbacher, G. (2017). Interpolation-based Model Checking and IC3. Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science, Znaim, Czechia. http://hdl.handle.net/20.500.12708/86685
  • Preface of the Special Issue in Memoriam Helmut Veith / Gottlob, G., Henzinger, T. A., & Weissenbacher, G. (2017). Preface of the Special Issue in Memoriam Helmut Veith. Formal Methods in System Design, 51(2), 267–269. https://doi.org/10.1007/s10703-017-0307-6
  • Proceedings of Formal Methods in Computer Aided Design, FMCAD 2017 / Stewart, D., & Weissenbacher, G. (Eds.). (2017). Proceedings of Formal Methods in Computer Aided Design, FMCAD 2017. FMCAD Inc. https://doi.org/10.15781/T2JS9HQ7C

2016

  • Abstraction and mining of traces to explain concurrency bugs / Tabaei Befrouei, M., Wang, C., & Weissenbacher, G. (2016). Abstraction and mining of traces to explain concurrency bugs. Formal Methods in System Design. https://doi.org/10.1007/s10703-015-0240-5
    Download: PDF (1.57 MB)
  • Error Invariants for Concurrent Traces / Holzer, A., Schwartz-Narbonne, D., Tabaei Befrouei, M., Weissenbacher, G., & Wies, T. (2016). Error Invariants for Concurrent Traces. In FM 2016: Formal Methods (pp. 370–387). Lecture Notes in Computer Science/Springer. https://doi.org/10.1007/978-3-319-48989-6_23
  • Vienna Verification Tool: IC3 for Parallel Software / Günther, H., Laarman, A., & Weissenbacher, G. (2016). Vienna Verification Tool: IC3 for Parallel Software. In M. Chechik & J.-F. Raskin (Eds.), Tools and Algorithms for the Construction and Analysis of Systems : 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings (pp. 954–957). Springer. https://doi.org/10.1007/978-3-662-49674-9_69
    Download: PDF (173 KB)
  • Labelled Interpolation Systems for Hyper-Resolution, Clausal, and Local Proofs / Schlaipfer, M., & Weissenbacher, G. (2016). Labelled Interpolation Systems for Hyper-Resolution, Clausal, and Local Proofs. Journal of Automated Reasoning, 57(1), 3–36. https://doi.org/10.1007/s10817-016-9364-6
  • Logical methods in automated hardware and software verification / Weissenbacher, G. (2016). Logical methods in automated hardware and software verification [Professorial Dissertation, Technische Universität Wien]. reposiTUm. http://hdl.handle.net/20.500.12708/158852
  • Interpolation algorithms and their applications in model checking / Weissenbacher, G. (2016). Interpolation algorithms and their applications in model checking. Automata, Logic and Games, Singapore, Non-EU. http://hdl.handle.net/20.500.12708/86305

2015

2014

  • Reduction of Resolution Refutations and Interpolants via Subsumption / Bloem, R., Malik, S., Schlaipfer, M., & Weissenbacher, G. (2014). Reduction of Resolution Refutations and Interpolants via Subsumption. In E. Yahav (Ed.), Hardware and Software: Verification and Testing : 10th International Haifa Verification Conference, HVC 2014, Haifa, Israel, November 18-20, 2014, Proceedings. Springer Cham. https://doi.org/10.1007/978-3-319-13338-6_15
    Download: PDF (408 KB)
  • Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR) / Birgmeier, J., Bradley, A. R., & Weissenbacher, G. (2014). Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR). In Computer Aided Verification (pp. 831–848). Springer / LNCS. https://doi.org/10.1007/978-3-319-08867-9_55
  • Incremental bounded software model checking / Günther, H., & Weissenbacher, G. (2014). Incremental bounded software model checking. In Proceedings of the 2014 International SPIN Symposium on Model Checking of Software. International SPIN Symposium on Model Checking of Software (SPIN), Stony Brook, NY, USA, Non-EU. ACM New York, NY, USA. https://doi.org/10.1145/2632362.2632374
  • Abstraction and Mining of Traces to Explain Concurrency Bugs / Tabaei Befrouei, M., Wang, C., & Weissenbacher, G. (2014). Abstraction and Mining of Traces to Explain Concurrency Bugs. In Runtime Verification (pp. 162–177). Springer / LNCS. https://doi.org/10.1007/978-3-319-11164-3_14
  • Silicon fault diagnosis using sequence interpolation with backbones / Zhu, C. S., Weissenbacher, G., & Malik, S. (2014). Silicon fault diagnosis using sequence interpolation with backbones. In ICCAD (pp. 348–355). IEEE Press Piscataway, NJ, USA. http://hdl.handle.net/20.500.12708/55310

2013

  • Under-Approximating Loops in C Programs for Fast Counterexample Detection / Kroening, D., Lewis, M., & Weissenbacher, G. (2013). Under-Approximating Loops in C Programs for Fast Counterexample Detection. In Computer Aided Verification (pp. 381–396). Springer / LNCS. https://doi.org/10.1007/978-3-642-39799-8_26
  • Advanced SAT Techniques for Abstract Argumentation / Wallner, J. P., Weissenbacher, G., & Woltran, S. (2013). Advanced SAT Techniques for Abstract Argumentation. In Computational Logic in Multi-Agent Systems 14th International Workshop, CLIMA XIV, Corunna, Spain, September 16-18, 2013, Proceedings (pp. 138–154). Springer / LNCS. https://doi.org/10.1007/978-3-642-40624-9_9

2012

  • Labelled Interpolation Systems / Weissenbacher, G. (2012). Labelled Interpolation Systems. Dagstuhl Seminar 12461: Games and Decisions for Rigorous Systems Engineering, Dagstuhl, Deutschland, EU. http://hdl.handle.net/20.500.12708/85433
  • Interpolant Strength Revisited / Weissenbacher, G. (2012). Interpolant Strength Revisited. In Theory and Applications of Satisfiability Testing – SAT 2012 (pp. 312–326). LNCS / Springer. https://doi.org/10.1007/978-3-642-31612-8_24
  • Coverage-Based Trace Signal Selection for Fault Localisation in Post-silicon Validation / Charlie Shucheng, Z., Weissenbacher, G., & Malik, S. (2012). Coverage-Based Trace Signal Selection for Fault Localisation in Post-silicon Validation. In Hardware and Software: Verification and Testing (pp. 132–147). Lecture Notes in Computer Science. Springer Verlag. https://doi.org/10.1007/978-3-642-39611-3_16
  • Parallel Assertions for Architectures with Weak Memory Models / Schwartz-Narbonne, D., Weissenbacher, G., & Malik, S. (2012). Parallel Assertions for Architectures with Weak Memory Models. In Automated Technology for Verification and Analysis (pp. 254–268). Lecture Notes in Computer Science. Springer Verlag. https://doi.org/10.1007/978-3-642-33386-6_21