2 citations · 2 across the 3 of their papers we have counts for
8 papers · 1 filter
On Verifying Designs With Incomplete Specification
Eugene Goldberg
Incompleteness of a specification creates two problems. First, an implementation of may have some properties tha…
Generation Of A Complete Set Of Properties
Eugene Goldberg
One of the problems of formal verification is that it is not functionally complete due the incompleteness of specifications. An implementation meeting an incomplete specification m…
Partial Quantifier Elimination With Learning
Eugene Goldberg
We consider a modification of the Quantifier Elimination (QE) problem called Partial QE (PQE). In PQE, only a small part of the formula is taken out of the scope of quantifiers. Th…
Improving Convergence Rate Of IC3
Eugene Goldberg
IC3, a well-known model checker, proves a property of a transition system by building a sequence of formulas . Formula , over-approximates the…
Quantifier Elimination With Structural Learning
Eugene Goldberg
We consider the Quantifier Elimination (QE) problem for propositional CNF formulas with existential quantifiers. QE plays a key role in formal verification. Earlier, we presented a…
Complete Test Sets And Their Approximations
Eugene Goldberg
We use testing to check if a combinational circuit always evaluates to 0 (written as ). We call a set of tests proving a complete test set (CTS). The c…