| 2023 | CAV | Partial Quantifier Elimination and Property Generation. | Eugene Goldberg |
| 2018 | DATE | Efficient verification of multi-property designs (The benefit of wrong assumptions). | Eugene Goldberg, Matthias Gdemann, Daniel Kroening, Rajdeep Mukherjee |
| 2018 | FMCAD | Complete Test Sets And Their Approximations. | Eugene Goldberg |
| 2016 | FMCAD | Equivalence checking by logic relaxation. | Eugene Goldberg |
| 2013 | FMCAD | Quantifier elimination via clause redundancy. | Eugene Goldberg, Panagiotis Manolios |
| 2012 | FMCAD | Quantifier elimination by Dependency Sequents. | Eugene Goldberg, Panagiotis Manolios |
| 2010 | TAP | Generating High-Quality Tests for Boolean Circuits by Treating Tests as Proof Encoding. | Eugene Goldberg, Panagiotis Manolios |
| 2009 | SAT | Boundary Points and Resolution. | Eugene Goldberg |
| 2008 | SAT | A Decision-Making Procedure for Resolution-Based SAT-Solvers. | Eugene Goldberg |
| 2008 | VMCAI | On Bridging Simulation and Formal Verification. | Eugene Goldberg |
| 2007 | DSD | On Complexity of Internal and External Equivalence Checking. | Eugene Goldberg, Kanupriya Gulati |
| 2007 | DSD | Toggle Equivalence Preserving (TEP) Logic Optimization. | Eugene Goldberg, Kanupriya Gulati, Sunil P. Khatri |
| 2006 | SAT | Determinization of Resolution by an Algorithm Operating on Complete Assignments. | Eugene Goldberg |
| 2005 | SAT | Equivalence Checking of Circuits with Parameterized Specifications. | Eugene Goldberg |
| 2003 | SAT | How Good Can a Resolution Based SAT-solver Be? | Eugene Goldberg, Yakov Novikov |
| 2002 | CADE | Testing Satisfiability of CNF Formulas by Computing a Stable Set of Points. | Eugene Goldberg |
| 2000 | VLSID | Timing Analysis with Implicitly Specified False Paths. | Eugene Goldberg, Alexander Saldanha |
| 1994 | FPL | Using Consensusless Covers for Fast Operating on Boolean Functions. | Eugene Goldberg, Ludmila Krasilnikova |