Himanshu Jain

Verification using Satisfiability Checking, Predicate Abstraction, and Craig Interpolation Degree Type: Ph.D. in Computer Science
Advisor(s): Edmund M. Clarke
Graduated: December 2008

Abstract:

Automatic verification of hardware and software implementations is crucial for building reliable computer systems. Most verification tools rely on decision procedures to check the satisfiability of various formulas that are generated during the verification process. This thesis develops new techniques for building efficient decision procedures and adds new capabilities to the existing decision procedures for certain logics.

Boolean satisfiability (SAT) solvers are used heavily in verification tools as decision procedures for propositional logic. Most state-of-the-art SAT solvers are based on the Davis-Putnam-Logemann-Loveland (DPLL) algorithm and require the input formula to be in Conjunctive Normal Form (CNF). However, typical formulas that arise in practice are non-clausal, that is, not in CNF. Converting a general formula to CNF introduces overhead in the form of new variables and may destroy the structure of the initial formula, which can be useful to check satisfiability efficiently. We present two non-clausal SAT algorithms that operate on the Negation Normal Form (NNF) of the given formula. The NNF of a formula is usually more succinct than the CNF of the formula. The first algorithm is based on the idea of General Matings developed by Andrews in 1981. We develop techniques for performing search space pruning, learning, non-chronological backtracking in the context of a General Matings based SAT solver. The second algorithm applies the DPLL algorithm to NNF formulas. We devise new algorithms for performing Boolean Constraint Propagation (BCP), a key task in the DPLL algorithm.

Most hardware verification tools convert a high level design into a low level representation called a netlist for verification. However, algorithms that operate at the netlist level are unable to exploit the structure of the higher abstraction levels such as register transfer level, and thus, are less scalable. This thesis proposes the use of predicate abstraction for verifying register transfer level (RTL) Verilog. Predicate abstraction is a technique introduced for software verification. There are two challenges when applying predicate abstraction to circuits: (i) The computation of the abstract model in the presence of a large number of predicates, and (ii) discovery of suitable word-level predicates for abstraction refinement. We address the first problem using a technique called predicate clustering. We address the second problem by computing weakest pre-conditions of Verilog statements in order to obtain new word-level predicates during abstraction refinement.

An alternative technique for finding new predicates for refinement is based on the computation of Craig interpolants. Efficient algorithms are known for computing interpolants in rational and real linear arithmetic. We focus on subsets of integer linear arithmetic. Our main results are polynomial time algorithms for obtaining proofs of unsatisfiability and interpolants for conjunctions of linear diophantine equations, linear modular equations (linear congruences), and linear diophantine disequations. We show the utility of our interpolation algorithms for discovering modular/divisibility predicates in a counterexample guided abstraction refinement (CEGAR) framework. This has enabled verification of simple programs that cannot be checked using existing CEGAR based model checkers.

Thesis Committee:
Edmund M. Clarke (Chair)
Randal E. Bryant
Frank Pfenning
Aarti Gupta (NEC Laboratories )
Kenneth L. McMillan (Cadence Berkeley Labs)

Peter Lee, Head, Computer Science Department
Randy Bryant, Dean, School of Computer Science

Keywords:
Formal methods, model checking, abstraction, refinement, bounded model checking, Boolean satisfiability, non-clausal SAT solvers, DPLL, general matings, unsatisfiable core, craig interpolation, proofs of unsatisfiability, linear diophantine equations, linear modular equations (linear congruences), linear diophantine disequations