GSRC Student Profile:
Research Overview: Satisfiability Checking of Non-clausal Formulas and Word-level Verification of Hardware Designs
I am working on the following projects:
Predicate Abstraction and Refinement techniques
for Verifying Verilog: Most model checkers used in
the hardware industry use a very low level design, usually a net-list, for verification. Our work develops techniques for verifying hardware designs at a higher level of abstraction. In particular, we use predicate abstraction, a
software verification technique, to verify register transfer level (RTL) circuits. A tool based on this work is available from
http://www.cs.cmu.edu/~modelcheck/vcegar. For more details see our IEEE TCAD 2007 paper (journal version) or DAC 2005 paper.
Non-clausal Satisfiability (SAT) solvers: We are developing new SAT
solvers that do not require the input formula to be in Conjunctive
Normal Form (CNF). Our first attempt in this direction is a solver
called SatMate. It is based on the idea of General Matings. We devised
techniques for performing search space pruning, learning, and
non-chronological backtracking in the new solver. On certain benchmark
classes our solver has a better performance than CNF-based SAT
solvers. For more details see our SAT 2006 paper.
Efficient support for Transactions in Concurrent Software: We are
developing new ideas to improve software transactional memory (STM)
implementations. We are also working on verification of programs that
use transactions and verification of transactional memory
implementations themselves.
Software verification using static analysis and model checking: We
used the invariants generated from abstract domains (octagon abstract
domain) to improve static analysis and verification of C programs. We
also developed techniques for improving the performance of the
predicate abstraction and refinement loop. The main idea was to
localize the use of predicates using weakest pre-conditions. For more
details see our CAV 2006 paper and TACAS 2005 paper.
Verification of SpecC Programs: We applied predicate abstraction for
verification of SpecC, a hardware/software system-level description
language. This involved dealing with the concurrency constructs and
the bit-vector semantics of the language. For more details see our
FMSD 2007 paper (journal version) or MEMOCODE 2004 paper.
You can obtain copies of my papers from my website . Please email me if a paper you are looking for is not available.
| 
