Eugene Goldberg

CoRR, 2024

2023

Verification Of Partial Quantifier Elimination.

[BibT_eX]

[DOI]

CoRR, 2023

Partial Quantifier Elimination and Property Generation.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 35th International Conference, 2023

2020

On Verifying Designs With Incomplete Specification.

[BibT_eX]

[DOI]

CoRR, 2020

Generation Of A Complete Set Of Properties.

[BibT_eX]

[DOI]

CoRR, 2020

Partial Quantifier Elimination By Certificate Clauses.

[BibT_eX]

[DOI]

CoRR, 2020

2019

Partial Quantifier Elimination With Learning.

[BibT_eX]

[DOI]

CoRR, 2019

2018

Quantifier Elimination With Structural Learning.

[BibT_eX]

[DOI]

CoRR, 2018

Improving Convergence Rate Of IC3.

[BibT_eX]

[DOI]

CoRR, 2018

Generation of complete test sets.

[BibT_eX]

[DOI]

CoRR, 2018

Complete Test Sets And Their Approximations.

[BibT_eX]

[DOI]

Proceedings of the 2018 Formal Methods in Computer Aided Design, 2018

Efficient verification of multi-property designs (The benefit of wrong assumptions).

[BibT_eX]

[DOI]

Proceedings of the 2018 Design, Automation & Test in Europe Conference & Exhibition, 2018

2017

Efficient Verification of Multi-Property Designs (The Benefit of Wrong Assumptions) (Extended Version).

[BibT_eX]

[DOI]

CoRR, 2017

2016

Property Checking Without Invariant Generation.

[BibT_eX]

[DOI]

CoRR, 2016

Property Checking By Logic Relaxation.

[BibT_eX]

[DOI]

CoRR, 2016

Equivalence checking by logic relaxation.

[BibT_eX]

[DOI]

Proceedings of the 2016 Formal Methods in Computer-Aided Design, 2016

2015

Equivalence Checking and Simulation By Computing Range Reduction.

[BibT_eX]

[DOI]

CoRR, 2015

2014

Quantifier elimination by dependency sequents.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2014

Bug Hunting By Computing Range Reduction.

[BibT_eX]

[DOI]

CoRR, 2014

Software for Quantifier Elimination in Propositional Logic.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Software - ICMS 2014, 2014

Partial Quantifier Elimination.

[BibT_eX]

[DOI]

Proceedings of the Hardware and Software: Verification and Testing, 2014

2013

Verification of Sequential Circuits by Tests-As-Proofs Paradigm.

[BibT_eX]

[DOI]

Mitesh Jain

CoRR, 2013

Quantifier elimination via clause redundancy.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 2013

2012

Checking Satisfiability by Dependency Sequents

[BibT_eX]

[DOI]

CoRR, 2012

Removal of Quantifiers by Elimination of Boundary Points

[BibT_eX]

[DOI]

CoRR, 2012

2010

Generating High-Quality Tests for Boolean Circuits by Treating Tests as Proof Encoding.

[BibT_eX]

[DOI]

Proceedings of the Tests and Proofs - 4th International Conference, 2010

SAT-Solving Based on Boundary Point Elimination.

[BibT_eX]

[DOI]

Proceedings of the Hardware and Software: Verification and Testing, 2010

2009

Boundary Points and Resolution.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2009

2008

A Resolution Based SAT-solver Operating on Complete Assignments.

[BibT_eX]

[DOI]

J. Satisf. Boolean Model. Comput., 2008

On Bridging Simulation and Formal Verification.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2008

A Decision-Making Procedure for Resolution-Based SAT-Solvers.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2008

2007

BerkMin: A fast and robust Sat-solver.

[BibT_eX]

[DOI]

Discret. Appl. Math., 2007

Toggle Equivalence Preserving (TEP) Logic Optimization.

[BibT_eX]

[DOI]

Kanupriya Gulati

Sunil P. Khatri

Proceedings of the Tenth Euromicro Conference on Digital System Design: Architectures, 2007

On Complexity of Internal and External Equivalence Checking.

[BibT_eX]

[DOI]

Kanupriya Gulati

Proceedings of the Tenth Euromicro Conference on Digital System Design: Architectures, 2007

2006

Determinization of Resolution by an Algorithm Operating on Complete Assignments.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2006

2005

Testing satisfiability of CNF formulas by computing a stable set of points.

[BibT_eX]

[DOI]

Ann. Math. Artif. Intell., 2005

Equivalence Checking of Circuits with Parameterized Specifications.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2005

On equivalence checking and logic synthesis of circuits with a common specification.

[BibT_eX]

[DOI]

Proceedings of the 15th ACM Great Lakes Symposium on VLSI 2005, 2005

2003

How Good Can a Resolution Based SAT-solver Be?

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2003

Verification of Proofs of Unsatisfiability for CNF Formulas.

[BibT_eX]

[DOI]

Proceedings of the 2003 Design, 2003

2002

Using Problem Symmetry in Search Based Satisfiability Algorithms.

[BibT_eX]

[DOI]

Mukul R. Prasad

Proceedings of the 2002 Design, 2002

2001

Proving unsatisfiability of CNFs locally.

[BibT_eX]

[DOI]

Electron. Notes Discret. Math., 2001

An efficient learning procedure for multiple implication checks.

[BibT_eX]

[DOI]

Proceedings of the Conference on Design, Automation and Test in Europe, 2001

Using SAT for combinational equivalence checking.

[BibT_eX]

[DOI]

Mukul R. Prasad

Proceedings of the Conference on Design, Automation and Test in Europe, 2001

2000

Negative thinking in branch-and-bound: the case of unate covering.

[BibT_eX]

[DOI]

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2000

Timing Analysis with Implicitly Specified False Paths.

[BibT_eX]

[DOI]

Alexander Saldanha

Proceedings of the 13th International Conference on VLSI Design (VLSI Design 2000), 2000

1999

Aura II: Combining Negative Thinking and Branch-and-Bound in Unate Covering Problems.

[BibT_eX]

Proceedings of the VLSI: Systems on a Chip, 1999

1998

Theory and algorithms for face hypercube embedding.

[BibT_eX]

[DOI]

Tiziano Villa

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1998

Combinational Verification based on High-Level Functional Specifications.

[BibT_eX]

[DOI]

Yuji Kukimoto

Proceedings of the 1998 Design, 1998

1997

A fast and robust exact algorithm for face embedding.

[BibT_eX]

[DOI]

Tiziano Villa

Proceedings of the 1997 IEEE/ACM International Conference on Computer-Aided Design, 1997

Negative thinking by incremental problem solving: application to unate covering.

[BibT_eX]

[DOI]

Proceedings of the 1997 IEEE/ACM International Conference on Computer-Aided Design, 1997

1994

Using Consensusless Covers for Fast Operating on Boolean Functions.

[BibT_eX]

[DOI]