Publications

In reverse chronological order.

2010

• Interpolant Strength
• Automatic Analysis of Scratch-pad Memory Code for Heterogeneous Multicore Processors
• Ranking Function Synthesis for Bit-Vector Relations
• Boom: Analyzing Boolean Programs with Unbounded Concurrency
• 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.
• Coverage in Interpolation-based Model Checking

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)

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
  This paper is at rank 7 on this list.
• 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
• Race Analysis for SystemC using Model Checking
  The SBMF 2009 proceedings contain an extended and revised version of this paper.
• 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

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
• Error Explanation with Distance Metrics
• 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.
• 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.

2001

• Automated Pipeline Design
  

2000

• Proving the Correctness of Pipelined Micro-Architectures
  

1999

• The Impact of Hardware Scheduling Mechanisms on the Performance and Cost of Processor Designs
  
• Proving the Correctness of Processors with Delayed Branch using Delayed PC
  This paper appreared previously at the HLVDT workshop.

Electronic versions of these papers are linked from the paper's page.