About me

Georg Weissenbacher's publications

Boolean Satisfiability Solvers: Techniques and Extensions
with Sharad Malik
In Tools for Analysis and Verification of Software Safety and Security, NATO Science for Peace and Security Series, IOS Press
Digitaltechnik - Eine praxisnahe Einführung
with Armin Biere, Daniel Kröning, and Christoph M. Wintersteiger
Springer textbook, March 2008
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
2012
Interpolant Strength Revisited
Proceedings of the 15th Conference on Theory and Applications of Satisfiability Testing (SAT)
Trento, Italy, June 2012 (to appear)
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
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.
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