Publications
In reverse chronological order. Electronic versions are linked from the paper's page.
2025
- Quantifying the Benefits of Code Hints for Refactoring Deprecated Java APIs
- Program Synthesis From Partial Traces
- Scalable, Validated Code Translation of Entire Projects using Large Language Models
2024
- Neural Model Checking
- Safeguarded Progress in Reinforcement Learning: Safe Bayesian Exploration for Control Policy Synthesis
-
Symbolic Task Inference in Deep Reinforcement
Learning
This is an extended version of a paper that appeared at AAAI 2021.
2023
- Certified Reinforcement Learning with Logic Guidance
- Synthesising Programs with Non-trivial Constants
This is an extended version of a paper that appeared at CAV 2018. - Enhancing active model learning with equivalence checking using simulation relations
This is an extended version of a paper that appeared at DATE 2022.
2022
2021
- Ranking Policy Decisions
- Explanations for Occluded Images
- Exposing Previously Undetectable Faults in Deep Neural Networks
- Shielding Atari Games with Bounded Prescience
- Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration
This is an extended (and corrected) version of a paper that appeared at SAS 2015.
2020
- Using Model Checking Tools to Triage the Severity of Security Bugs in the Xen Hypervisor
- Explaining Image Classifiers using Statistical Fault Localization
- The Taint Rabbit: Optimizing Generic Taint Analysis with Dynamic Fast Path Generation
- Learning Concise Models from Long Execution Traces
- Learning the Language of Software Errors
This is an extended version of an ATVA 2015 paper. - Cautious Reinforcement Learning with Logical Constraints
- Automated Formal Synthesis of Provably Safe Digital Controllers for Continuous Plants
This is an extended variant of a paper that appeared at CAV 2017. - Model Checking Boot Code from AWS Data Centers
This is an extended variant of a paper that appeared at CAV 2018.
2019
- Gollum: Modular and Greybox Exploit Generation for Heap Overflows in Interpreters
- Reinforcement Learning for Temporal Logic Control Synthesis with Probabilistic Satisfaction Guarantees
- Global Robustness Evaluation of Deep Neural Networks with Provable Guarantees for the Hamming Distance
- Generating Realistic Unrestricted Adversarial Inputs using Dual-Objective GAN Training
- Logically-Constrained Neural Fitted Q-Iteration
- DeepConcolic: Testing and Debugging Deep Neural Networks
- Structural Test Coverage Criteria for Deep Neural Networks
A poster was presented at ICSE.
2018
- Concolic Testing for Deep Neural Networks
- Automatic Heap Layout Manipulation for Exploitation
- JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode
- Verification of Tree-Based Hierarchical Read-Copy Update in the Linux Kernel
- Efficient Verification of Multi-Property Designs (best paper in the design track)
- Program Synthesis for Program Analysis
This is an extended version of a paper that appeared at LPAR 2015. - DSValidator: An Automated Counterexample Reproducibility Tool for Digital Systems
- Optimising Spectrum Based Fault Localisation for Single Fault Programs using Specifications
- Effective Verification for Low-Level Software with Competing Interrupts
This is an extended version of a paper that appeared at DATE 2015. - Bit-Precise Procedure-Modular Termination Analysis
This is an extended version of a paper that appeared at ASE 2015.
2017
- Functional Requirements-Based Automated Testing for Avionics
- DSSynth: An Automated Digital Controller Synthesis Tool for Physical Plants
- Verifying Digital Systems with MATLAB
- Lifting CDCL to Template-based Abstract Domains for Program Verification
- Modular Demand-Driven Analysis of Semantic Difference for Program Versions
- Sound Numerical Computations in Abstract Acceleration
- Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants
- Abstract Interpretation with Unfoldings
- Program Synthesis: Challenges and Opportunities
- Independence Abstractions and Models of Concurrency
- Formal Techniques for Effective Co-verification of Hardware/Software Co-designs
- Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants
- Incremental Bounded Model Checking for Embedded Software
- Don't Sit on the Fence: A Static Analysis Approach to Automatic Fence Insertion
This is an extended version of a CAV 2014 paper. - Lost in Abstraction: Monotonicity in Multi-Threaded Programs
This is an extended version of a paper that appeared at CONCUR 2014. - Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs
This is an extended version of a paper that appeared at FM 2014.
2016
- Probabilistic Fault Localisation
- Danger Invariants
- Equivalence Checking of a Floating-point Unit Against a High-level C Model
- Sound Static Deadlock Analysis for C/Pthreads
- Static Program Analysis for Identifying Energy Bugs in Graphics-Intensive Mobile Apps
- Verification of Concurrent Software
- Assisted Coverage Closure
- 2LS for Program Analysis
- The Virtues of Conflict: Analysing Modern Concurrency
- v2c – A Verilog to C Translator Tool
- Formalizing and Checking Thread Refinement for Data-Race-Free Execution Models
- Automatic Generation of Propagation Complete SAT Encodings
- Unbounded Safety Verification for Hardware Using Software Analyzers
- Generating test case chains for reactive systems
This is an extended version of an ICTSS 2013 paper.
2015
- Accelerating Invariant Generation
- Unfolding-based Partial Order Reduction (best paper award)
- From AgentSpeak to C for Safety Considerations in Unmanned Aerial Vehicles
- Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration
- Safety Verification and Refutation by k-Invariants and k-Induction
- Hardware Verification using Software Analyzers
- Equivalence Checking using Trace Partitioning
- Successful Use of Incremental BMC in the Automotive Industry
- On Partial Order Semantics for SAT/SMT-based Symbolic Encodings of Weak Memory Concurrency
- Faster Linearizability Checking via P-Compositionality
- Under-Approximating Loops in C Programs for Fast Counterexample Detection
This is an extended version of a CAV 2013 paper. - Property-Driven Fence Insertion using Reorder Bounded Model Checking
- Proving Safety with Trace Automata and Bounded Model Checking
- Propositional Reasoning about Safety and Termination of Heap-Manipulating Programs
- Unrestricted Termination and Non-Termination Arguments for Bit-Vector Programs
- Evaluation of Measures for Statistical Fault Localisation and an Optimising Scheme
- Verifying synchronous reactive systems using lazy abstraction
2014
- Automating Software Analysis at Large Scale
- Accelerated Test Execution using GPUs
- A Widening Approach to Multi-Threaded Program Verification
- Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs
- Deciding Floating-Point Logic with Abstract Conflict Driven Clause Learning
This is an extended version of an FMCAD 2012 paper. - Component-based Design and Verification in X-MAN
- Model and Proof Generation for Heap-Manipulating Programs
- Abstract Satisfaction
- CBMC – C Bounded Model Checker
- Problem Solving for the 21st Century
2013
- Verifying Multi-threaded Software with Impact
- Formal Co-Validation of Low-Level Hardware/Software Interfaces
- Interpolation-Based Verification of Floating-Point Programs with Abstract CDCL
- A Visual Studio Plug-In for CProver
- Partial Orders for Efficient Bounded Model Checking of Concurrent Software
- Abstract Conflict Driven Learning
- An Abstract Interpretation of DPLL(T)
- Abstraction of Syntax
- Software Verification for Weak Memory via Program Transformation
- Counterexample Guided Precondition Inference
- Ranking Function Synthesis for Bit-Vector Relations
This is an extended version of a TACAS 2010 paper. - Loop Summarization using State and Transition Invariants
This is an extended version of a TACAS 2011 paper
2012
- Satisfiability Solvers are Static Analyzers
- Efficient Coverability Analysis by Proof Minimization
- Numeric Bounds Analysis with Conflict-Driven Learning
- Computing Mutation Coverage in Interpolation-based Model Checking
This is an extended version of a DAC 2010 paper. - Counterexample-Guided Abstraction Refinement for Symmetric Concurrent Programs
This is an extended version of a CAV 2011 paper.
2011
- An Interpolating Sequent Calculus for Quantifier-free Presburger Arithmetic
This is an extended version of a conference paper. - Soundness of Data Flow Analyses for Weak Memory Models
- Making Software Verification Tools Really Work
- Software Verification Using k-Induction
- Automatic Analysis of DMA Races Using Model Checking and k-induction
- Interpolation-based Software Verification with WOLVERINE
- Linear Completeness Thresholds for Bounded Model Checking
- Test-Case Generation for Embedded Simulink via Formal Concept Analysis
- Strengthening Induction-Based Race Checking with Lightweight Static Analysis
- Beyond Quantifier-free Interpolation in Extensions of Presburger Arithmetic
- SCRATCH: a tool for automatic analysis of DMA races
2010
- Tightening Test Coverage Metrics: A Case Study in Equivalence Checking using k-Induction
- Interpolant Strength
- Automatic Analysis of Scratch-pad Memory Code for Heterogeneous Multicore Processors
- Boom: Taking Boolean program model checking one step further
- Periodic Orbits and Equilibria in Glass Models for Gene Regulatory Networks
- Verification and Falsification of Programs with Loops using Predicate Abstraction
A previous version of this paper has appeared at CAV. - Termination Analysis with Compositional Transition Invariants
- Dynamic Cutoff Detection in Parameterized Concurrent Programs
- Race Analysis for SystemC using Model Checking
This work has first appeared in an ICCAD 2008 paper; an extension has appeared in an SBMF 2009 invited paper. - Context-Aware Counter Abstraction
- Interpolating Quantifier-Free Presburger Arithmetic
2009
- Deciding Bit-Vector Arithmetic with Abstraction
A previous version of this paper has appeared at TACAS. - Strengthening Properties using Abstraction Refinement
- Fixed Points in Multi-Cycle Path Detection
- A Framework for Satisfiability Modulo Theories
- Symbolic Counter Abstraction for Concurrent Software
- A Propositional Encoding of Lean Induced Cycles in Binary Hypercubes
- Loopfrog: A Static Analyzer for ANSI-C Programs
- Mixed Abstractions for Floating-Point Arithmetic
- An Interpolating Decision Procedure for Transitive Relations with Uninterpreted Functions
- Software Verification (this is a book chapter in the Handbook of Satisfiability)
- Speeding up Simulation of SystemC using Model Checking (invited)
- Mutation-based Test Case Generation for Simulink Models
2008
- Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog
A previous version of this paper appeared at DAC 2005.
An earlier version of this paper is also available as CMU technical report. - Approximation Refinement for Interpolation-Based Model Checking
- Formal Verification at Higher Levels of Abstraction
- Scoot: A Tool for the Analysis of SystemC Models
- A Survey of Automated Techniques for Formal Software Verification
- Computing Binary Combinatorial Gray Codes via Exhaustive Search with SAT-Solvers
An extended version of this paper is available as ETH Technical Report. - Classification of Hamiltonian Cycles in the 6-Cube
- Loop Summarization using Abstract Transformers
- An Efficient SAT Encoding of Circuit Codes
2007
- Verification of SpecC using Predicate Abstraction
A previous version of this paper appeared at MEMOCODE 2004 - Image Computation and Predicate Refinement for RTL Verilog using Word Level Proofs
- VCEGAR: Verilog CounterExample Guided Abstraction Refinement
- A First Step Towards a Unified Proof Checker for QBF
- An Algebraic Algorithm for the Identification of Glass Networks with Periodic Orbits along Cyclic Attractors
- SAT-based Summarisation for Boolean Programs
- Model Checking with Abstraction for Web Services
- Verification of Boolean Programs with Unbounded Thread Creation
A previous version of this paper appeared at FMCAD 2006. - Lifting Propositional Interpolants to the Word-Level
- Static Analysis to Enhance the Power of Model Checking for Concurrent Software
- Verifying C++ with STL Containers via Predicate Abstraction
- Model Checking Concurrent Linux Device Drivers
- A Complete Bounded Model Checking Algorithm for Pushdown Systems
2006
- Putting it all together - Formal Verification of the VAMP
- Approximating Predicate Images for Bit-Vector Logic
- Decision Procedures for the Grand Challenge
- ExpliSAT: Guiding SAT-Based Software Verification with Explicit States
- Error Explanation with Distance Metrics
2005
- Computational Challenges in Bounded Model Checking
- SATABS: SAT-based Predicate Abstraction for ANSI-C
- Cogent: Accurate theorem proving for program verification
A full version of this paper is available in the Post-Proceedings of ISoLA 2004 - Formal Verification of SystemC by Automatic Hardware/Software Partitioning
- Symbolic model checking for asynchronous Boolean programs
A previous version of this paper is available as ETH Technical Report. - Computing Over-Approximations with Bounded Model Checking
A previous version of this paper is available as ETH Technical Report.
2004
- Completeness and Complexity of Bounded Model Checking
- A Tool for Checking ANSI-C Programs
- Predicate Abstraction of ANSI-C Programs using SAT
A previous version of this paper is also available as CMU technical report.
A short version of this paper appeared previously at a DSN workshop. - Fault Tolerance Tradeoffs in Moving from Decentralized to Centralized Embedded System Architectures
- A SAT-Based Algorithm for Reparameterization in Symbolic Simulation
A previous version of this paper is also available as CMU technical report. - Understanding Counterexamples with explain
- Bounded Model Checking and Inductive Verification of Hybrid Discrete-continuous Systems
- Abstraction-based Satisfiability Solving of Presburger Arithmetic
A previous version of this paper is also available as CMU technical report. - Experiments with SAT-Based Symbolic Simulation Using Reparameterization in the Abstraction Refinement Framework
- Making the Most of BMC Counterexamples
- Checking Consistency of C and Verilog using Predicate Abstraction and Induction
A previous version of this paper is also available as CMU technical report. - Counterexample Guided Abstraction Refinement via Program Execution
2003
- Efficient Computation of Recurrence Diameters
- Hardware Verification using ANSI-C Programs as a Reference
- Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking
A long version of this paper is available as CMU Technical Report. This is the first conference paper to use CBMC. - Specifying and Verifying Systems with Multiple Clocks
- Using SAT based Image Computation for Reachability Analysis
- Instantiating uninterpreted functional units and memory system: functional verification of the VAMP processor
2002
- Application Specific Higher Order Logic Theorem Proving
- Formal Verification of Pipelined Microprocessors
This paper is a summary of my thesis.