About me

Georg Weissenbacher's publications

Boolean Satisfiability Solvers: Techniques and Extensions
with Sharad Malik
In Software Safety and Security - Tools for Analysis and Verification, NATO Science for Peace and Security Series, IOS Press, 2012
Digitaltechnik - Eine praxisnahe Einführung
with Armin Biere, Daniel Kröning, and Christoph M. Wintersteiger
Springer textbook, March 2008
2016
Labelled Interpolation Systems for Hyper-Resolution, Clausal, and Local Proofs
with Matthias Schlaipfer
Journal of Automated Reasoning, February 2016
Abstraction and mining of traces to explain concurrency bugs
with Mitra Tabaei Befrouei and Chao Wang
Formal Methods in Systems Design, January 2016
2015
Boolean Satisfiability Solvers and Their Applications in Model Checking
with Yakir Vizel and Sharad Malik
Proceedings of the IEEE, November 2015
Under-approximating loops in C programs for fast counterexample detection
with Daniel Kröning and Matt Lewis
Formal Methods in Systems Design, Springer, April 2015
2010
Verification and Falsification of Programs with Loops Using Predicate Abstraction
with Daniel Kröning
Formal Aspects of Computing, Springer, March 2010
2008
A Survey of Automated Techniques for Formal Software Verification
with Vijay D'Silva and Daniel Kröning
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Volume 27, Issue 7, July 2008
2017
Dynamic Reductions for Model Checking Concurrent Software
Proceedings of the 18th International Conference on Verification, Model Checking, And Abstract Interpretation (VMCAI)
with Henning Günther, Alfons Laarman, and Ana Sokolova
Paris, January 2017
2016
Error Invariants for Concurrent Traces
Proceedings of the 21st International Symposium on Formal Methods (FM)
with Andreas Holzer, Daniel Schwartz-Narbonne, Mitra Tabaei Befrouei, and Thomas Wies
Cyprus, November 2016
Vienna Verification Tool: IC3 for Parallel Software
(software verification competition contribution)
with Henning Günther and Alfons Laarman
Proceedings of the 22nd Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)
Eindhoven, Netherlands, April 2016
2015
Proving Safety with Trace Automata and Bounded Model Checking
Proceedings of the 20th International Symposium on Formal Methods (FM)
with Daniel Kroening and Matt Lewis
Oslo, Norway, June 2015
2014
Silicon Fault Diagnosis Using Sequence Interpolation with Backbones
Proceedings of the 33rd International Conference on Computer-Aided Design (ICCAD)
with Charlie Shucheng Zhu and Sharad Malik
San Jose, CA, November 2014
Reduction of Resolution Refutations and Interpolants via Subsumption
Proceedings of the 10th Haifa Verification Conference (HVC)
with Roderick Bloem, Sharad Malik, and Matthias Schlaipfer
Haifa, Israel, November 2014
Abstraction and Mining of Traces to Explain Concurrency Bugs
Proceedings of the 14th International Conference on Runtime Verification (RV)
with Mitra Tabaei Befrouei and Chao Wang
Toronto, Canada, September 2014
Incremental Bounded Software Model Checking
Proceedings of the 14th International SPIN Symposium on Model Checking of Software (SPIN)
with Henning Günther
San Jose, CA, July 2014
Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR)
Proceedings of the 26th Conference on Computer Aided Verification (CAV)
with Johannes Birgmeier and Aaron Bradley
Vienna, Austria, July 2014
2013
Under-Approximating Loops in C Programs for Fast Counterexample Detection
Proceedings of the 25th Conference on Computer Aided Verification (CAV)
with Daniel Kroening and Matt Lewis
St. Petersburg, Russia, July 2013
2012
Coverage-based Trace Signal Selection for Fault Localisation in Post-Silicon Validation
Proceedings of the 8th Haifa Verification Conference (HVC)
with Charlie Shucheng Zhu and Sharad Malik
Haifa, Israel, November 2012
Parallel Assertions for Architectures with Weak Memory Models
Proceedings of the 10th International Symposium on Automated Technology for Verification and Analysis (ATVA)
with Daniel Schwartz-Narbonne and Sharad Malik
Trivandrum, Kerala, October 2012
Interpolant Strength Revisited
Proceedings of the 15th Conference on Theory and Applications of Satisfiability Testing (SAT)
Trento, Italy, June 2012
Wolverine: Battling Bugs with Interpolants
(software verification competition contribution)
with Sharad Malik and Daniel Kröning
Proceedings of the 18th Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)
Talinn, Estonia, April 2012
2011
Post-Silicon Fault Localisation Using Maximum Satisfiability and Backbones
with Charlie Shucheng Zhu and Sharad Malik
Proceedings of the 11th Conference on Formal Methods in Computer Aided Design (FMCAD)
Austin, TX, November 2011
Also presented at the CESCA seminar at Virginia Tech in October 2011. Watch video.
Interpolation-based Software Verification with Wolverine
(tool paper)
with Daniel Kröning
Proceedings of the 23rd Conference on Computer Aided Verification (CAV)
Snowbird, UT, July 2011
Download the software model checker Wolverine.
2010
Interpolant Strength
with Vijay D'Silva, Daniel Kröning, and Mitra Purandare
Proceedings of Verification, Model Checking and Abstract Interpretation (VMCAI)
Madrid, Spain, January 2010
An extended version of this paper is available as ETH Zurich Technical Report.
Download slides.
2009
Mutation-based Test Case Generation for Simulink Models
with Angelo Brillout, Nannan He, Michele Mazzucchi, Daniel Kröning, Mitra Purandare, and Philipp Rümmer
Post-proceedings of Formal Methods for Components and Objects (FMCO), November 2010
Eindhoven, The Netherlands, November 2009
An Interpolating Decision Procedure for Transitive Relations with Uninterpreted Functions
with Daniel Kröning
Post-proceedings of the 5th Haifa Verification Conference (HVC)
Haifa, Israel, October 2009
This work was also presented at the UNU-IIST seminar in Macau in January, 2010.
Download slides.
2007
A Complete Bounded Model Checking Algorithm for Pushdown Systems
with Gérard Basler and Daniel Kröning
Proceedings of the 3rd Haifa Verification Conference (HVC)
Haifa, Israel, October 2007
Lifting Propositional Interpolants to the Word-Level
with Daniel Kröning
Proceedings of the 7th Conference on Formal Methods in Computer Aided Design (FMCAD)
Austin, TX, November 2007
Model Checking Concurrent Linux Device Drivers
(tool paper)
with Thomas Witkowski, Nicolas Blanc, and Daniel Kröning
Proceedings of the 22nd IEEE/ACM International Conference on Automated Software Engineering (ASE)
Atlanta, GA, November 2007
Download the DDVerify verification tool.
2006
Counterexamples with Loops for Predicate Abstraction
with Daniel Kröning
Proceedings of the 18th Conference on Computer Aided Verification (CAV)
Seattle, WA, August 2006
2005
From requirements to deployment: Verify that the right things are done correctly. The DECOS test bench
with Wolfgang Herzner and Erwin Schoitsch
Proceedings of the 8th International IEEE Conference on Intelligent Transportation Systems (ITSC)
Vienna, Austria, September 2005
Counterexample-Driven Abstraction Refinement: A pattern for Formal Verification of Large Systems
with Wolfgang Herzner
Proceedings of the 10th European Conference on Pattern Languages of Programs (EuroPLoP)
Irsee, Germany, July 2005
2013
Advanced SAT Techniques for Abstract Argumentation
with Johannes P. Wallner and Stefan Woltran
Proceedings of the 14th International Workshop on Computational Logic in Multi-Agent Systems (CLIMA XIV)
A Coruña, Spain, September 2013
2011
SAT-based Techniques for Determining Backbones for Post-Silicon Fault Localisation
with Charlie Shucheng Zhu, Divjyot Sethi, and Sharad Malik
Proceedings of the 16th IEEE International High Level Design Validation and Test Workshop (HLDVT)
Napa Valley, CA, November 2011
2007
SAT-based Summarization for Boolean Programs
with Gérard Basler and Daniel Kröning
Proceedings of the 14th International SPIN Workshop on Model Checking Software (SPIN)
Berlin, Germany, July 2007
2005
Allocation of Dependable Software Modules under Consideration of Replicas
with Egbert Althammer and Wolfgang Herzner
Proceedings of the First ERCIM Workshop on Software-Intensive Dependable Embedded Systems
Porto, Portugal, August 2005
Drum prüfe: Model Checking: Bugs in C-Programmen finden
with Daniel Kröning
Magazin für professionelle Informationstechnik, iX 5/2009
Abstrakte Kunst: Fehler finden mit Model-Checkern
Magazin für professionelle Informationstechnik, iX 5/2004
Ohne Beweis: VDM++, Lightweight Formal Methods
Magazin für professionelle Informationstechnik, iX 3/2001
A Proposal for a Theory of Finite Sets, Lists, and Maps for the SMT-Lib Standard
with Daniel Kröning and Philipp Rümmer
7th International Workshop on Satisfiability Modulo Theories (SAT)
Montreal, Canada, August 2009 (co-located with CADE)
In informal workshop proceedings.
Restructuring Resolution Refutations for Interpolation
with Vijay D'Silva, Daniel Kröning and Mitra Purandare
Technical report, Oxford University 2008.
Logical Methods in Automated Hardware and Software Verification
Habilitation thesis
TU Wien, Faculty of Informatics, July 2016
Program Analysis with Interpolants
Doctoral dissertation
Oxford University, Computing Laboratory, September 2010
An Abstraction/Refinement Scheme for Model Checking C Programs
Diplomarbeit (master's thesis)
Graz University of Technology, March 2003