2 citations · 2 across the 4 of their papers we have counts for
4 papers · 1 filter
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…
Generation of complete test sets
Eugene Goldberg
We use testing to check if a combinational circuit N always evaluates to 0. The usual point of view is that to prove that N always evaluates to 0 one has to check the value of N fo…