Formally proving that your design is incorrect
Speaker: Eugene Goldberg, Northeastern University
Date: Thursday, May 31 2012
Time: 1:30PM to 2:30PM
Location: 32-D463 (Star)
Host: Daniel Jackson, MIT-CSAIL
Contact: Maria Rebelo, 253-5895, mr@csail.mit.edu
Abstract: In practice, proving that a design is faulty comes down to showing that an input (test) produces the wrong result. However, finding an explicit test may be much harder than just showing that it exists. In terms of SAT-solving, to generate a test, one needs to find an assignment satisfying a CNF formula F(X). To prove that a test exists, it is sufficient to show that the formula Exists(X).F(X) is true. I will refer to the latter problem as Quantified SAT (QSAT).
In this talk, I will introduce the machinery of Dependency sequents (D-sequents) meant for solving QSAT and similar problems like quantifier elimination. A D-sequent is a record saying that some variables of X are redundant in Exists(X).F(X) under an assignment of values to some other variables of X. Solving Exists(X).F(X) comes down to derivation of a D-sequent stating that the variables of X are unconditionally redundant in Exists(X).F(X). If derivation of such a D-sequent does not require adding an empty clause to F, then F is satisfiable. Importantly, proving satisfiability of F does not require finding a satisfying assignment. I will describe an algorithm of quantifier elimination based on D-sequents and give experimental results of applying this algorithm to model checking problems. I will also show results of some preliminary experiments with a QSAT-solver based on D-sequents.
Bio: Eugene Goldberg graduated from the Belarusian State University as a theoretical physicist. He got his PhD degree in computer science from the Belarusian Academy of Science. He did his postdoc research at the University of California at Berkeley. For 11 years, he worked at Berkeley Research Labs of Cadence Design Systems as a research scientist. Currently, Eugene Goldberg is a researcher at Northeastern University. His interests are efficient algorithms for computationally hard problems with the emphasis on hardware/software synthesis, testing and formal verification.
See other events happening in May 2012
