Post-silicon Fault Localization
with Satisfiability Solvers
with Sharad Malik
In Post-Silicon Validation and
Debug, Prabhat Mishra and Farima Farahmandi (editors),
Springer 2018
CAV'18: Proceedings of the 30th
Conference on Computer Aided Verification
with Hana Chockler
Lecture Notes in Computer Science
10981 & 10982, Oxford, UK, July 14-17, 2018
(visit
CAV'18 webpage)
FMCAD'17: Proceedings of the 17th
Conference on Formal Methods in Computer-Aided Design
with Daryl Stewart
Formal Method in Computer-Aided Design
(FMCAD), Vienna, Austria, October 2-6, 2017
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
2021
Preface of the Special Issue on the Conference on Computer-Aided Verification 2018
with Hana Chockler
Formal Methods in System Design
Rely-guarantee bound analysis of parameterized concurrent shared-memory programs
with Thomas Pani and Florian Zuleger
Formal Methods in System Design
Preface of the Special Issue on the Conference on Formal Methods in Computer-Aided Design 2017
with Daryl Stewart
Formal Methods in System Design
Mutation Testing with Hyperproperties
with Andreas Fellner and Mitra Tabaei Befrouei
Software and Systems Modeling
2020
Extracting Safe Thread Schedules from Incomplete Model Checking Results
with Patrick Metzler and Neeraj Suri
International Journal on Software Tools for Technology Transfer
2019
Model-based, Mutation-driven Test-case Generation Via Heuristic-guided Branching Search
with Andreas Fellner, Willibald Krenn, Rupert Schlick, and Thorsten Tarrach
ACM Transactions on Embedded Computing Systems (TECS)
2018
Randomized Testing of Distributed
Systems with Probabilistic Guarantees
with Burcu Kulahcioglu Ozkan, Rupak
Majumdar, Filip Nikšić, and Mitra Tabaei Befrouei
Proceedings of the ACM on
Programming Languages (OOPSLA)
OOPSLA'18 Distinguished Paper Award
2017
Preface of the Special Issue in Memoriam Helmut Veith
with Georg Gottlob and Thomas A. Henzinger
Formal Methods in System Design,
volume 52, issue 2, November 2017
(guest editor
of FMSD
Special Issue in Memoriam Helmut Veith)
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
2023
A Formalization of Heisenbugs and Their Causes
Software Engineering and Formal Methods (SEFM 2023)
with Sarah Sallinger and Florian Zuleger
2021
Model Checking AUTOSAR Components with CBMC
Formal Methods in Computer-Aided Design (FMCAD 2021)
with Timothee Durand, Katalin Fazekas, and Jakob Zwirchmayr
Bounded Model Checking of Speculative Non-Interference
International Conference on
Computer-Aided Design (ICCAD 2021)
with Emmanuel Pescosta and Florian Zuleger
2020
Multi-linear Strategy Extraction for QBF Expansion Proofs via Local Soundness
Formal Methods in Computer-Aided Design (FMCAD 2020)
with Thomas Pani and Florian Zuleger
Multi-linear Strategy Extraction for QBF Expansion Proofs via Local Soundness
23rd International Conference on
Theory and Applications of Satisfiability Testing (SAT)
with Matthias Schlaipfer, Friedrich
Slivovsky, and Florian Zuleger
June 2020
RAT Elimination
Proceedings of the 23rd
International Conference on Logic for Programming,
Artificial Intelligence and Reasoning (LPAR)
with Adrián Rebola Pardo
May 2020
Language Inclusion for Finite Prime Event Structures
Proceedings of the 21st
International Conference on Verification, Model Checking
and Abstract Interpretation (VMCAI)
with Andreas Feller and Thorsten Tarrach
New Orleans, January 2020
2019
Mutation Testing with Hyperproperties
Proceedings of the 17th
International Conference on Software Engineering
and Formal Methods (SEFM)
with Andreas Feller and Mitra Tabaei Befrouei
Oslo, September 2019
Model-Based Diagnosis with
Multiple Observations
Proceedings of the 28th
International Joint Conference on Artificial Intelligence (IJCAI)
with Alexey Ignatiev, António Morgado and João Marques-Silva
Macau, August 2019
Extracting Safe Thread Schedules
from Incomplete Model Checking Results
Proceedings of the 26th
International SPIN Symposium on Model Checking Software (SPIN)
with Patrick Metzler and Neeraj Suri
Beijing, July 2019
2018
Rely-Guarantee Reasoning for
Automated Bound Analysis of Lock-Free Algorithms
Proceedings of the 18th
Conference on Formal Methods in Computer Aided Design (FMCAD)
with Thomas Pani and Florian Zuleger
Austin, October/November 2018
A Separation Logic with Data: Small
Models and Automation
Proceedings of the 9th
International Conference on Automated Reasoning (IJCAR)
with Jens Katelaan and Dejan Jovanovic
Oxford, July 2018
2017
Model-based, mutation-driven test case generation via heuristic-guided branching search
Proceedings of the 15th
International Conference on Formal Methods and Models for
System Design (MEMOCODE)
with Andreas Fellner, Willibald Krenn, Thorsten Tarrach, and Rupert Schlick
Vienna, September 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
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
arXiv
article arXiv:1410.5764
[cs.FL]
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
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
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
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