DEPARTMENT RESEARCH ACADEMICS PEOPLE NEWS
Rice Computer Science		SEARCH:
Rice University Department of Computer Science presents Clark Barrett Stanford University Automated Decision Procedures: A General-Purpose Verification Solution Abstract As digital designs increase in size and complexity to meet the relentless demands of Moore's Law, the difficulty of verifying the correctness of these designs has grown exponentially. Verification has become the primary challenge facing design teams today, dominating as much as two-thirds of the design cycle. Formal and semi-formal verification techniques offer a solution which requires more initial effort and expertise, but which is ultimately much more scalable than conventional verification methods. Such verification techniques are now receiving unprecedented attention from industry, and are quickly coming to be regarded as essential in the future of design verification. This talk will focus on a particular verification approach which is broadly applicable. The approach consists of using first-order logic to model verification properties and then using automated decision procedures to either prove the properties or provide counter-examples. I will present several advances in the theory and implementation of such decision procedures, developed as part of ongoing efforts to improve the Stanford Validity Checker. The more theoretical portion of the talk will address the general problem of combining satisfiability procedures for individual theories into a satisfiability procedure for the combined theory, a critical capability for producing general-purpose decision procedures. After reviewing the two conventional approaches, those of Shostak and of Nelson and Oppen, I will show how to combine the two methods to obtain the generality of the Nelson-Oppen method while retaining the efficiency of the Shostak method. The more practical portion of the talk will focus on the heuristic search problem that is inherent in trying to prove large formulas. I will present a technique that incorporates a state-of-the-art SAT solver (CHAFF) to dramatically increase performance. Results on processor verification benchmarks show that this technique can speed up the search by several orders of magnitude. Thursday, April 18, 2002 at 4:00 in DH 1064 Reception at 3:30 in DH3092 Clark Barrett is a faculty candidate. About Clark Barrett Clark Barrett received the B.S. degree from Brigham Young University in 1995, the M.S. in 1998 from Stanford, and the Ph.D. degree is expected in 2002 also from Stanford. He was a Co-valedictorian at Brigham Young and the recipient of the Karl G. Maeser Graduate Fellowship and a NDSEG fellowship. His research interests include cooperating decision procedures, formal and semi-formal verification of hardware, propositional satisfiability algorithms, and first-order logic and its applications. Copyright 2000 Rice University site problems: www@cs.rice.edu --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- ---