TU Wien Informatics

20 Years

About

Automated Software Verification

Roles

2024

  • Finding counterexamples to ∀∃ hyperproperties / Nießen, T., & Weissenbacher, G. (2024, January 16). Finding counterexamples to ∀∃ hyperproperties [Conference Presentation]. Formal Methods for Incorrectness 2024, London, United Kingdom of Great Britain and Northern Ireland (the). https://doi.org/10.34726/5455
    Download: Extended abstract (432 KB)

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
    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)
  • 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
  • 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, Deutschland, EU. IEEE. https://doi.org/10.1109/iccad51958.2021.9643462

2020

2019

  • 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
  • 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
  • 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 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, China, Non-EU. https://doi.org/10.24963/ijcai.2019/155

2018

  • 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
  • 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
  • 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, OR, USA, Non-EU. 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
  • 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

  • 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
  • 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, Tschechien, EU. http://hdl.handle.net/20.500.12708/86685
  • 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
  • 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, Vienna, Austria, EU. ACM. https://doi.org/10.1145/3127041.3127049
  • 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 Lecture Notes in Computer Science (pp. 246–265). Springer. https://doi.org/10.1007/978-3-319-52234-0_14

2016

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 Hardware and Software: Verification and Testing. 10th International Haifa Verification Conference, HVC 2014, Haifa, Israel, November 18-20, 2014 ; Yahav, Eran. 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

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