Papers and talks

2024

E. Goldberg. On efficient algorithms for partial quantifier elimination arXiv:2406.01307 [cs.LO]

E. Goldberg. Structure-aware computing by partial quantifier elimination arXiv:2403.05928 [cs.LO]

2023

E. Goldberg. Partial quantifier elimination and property generation, CAV-23, Paris, France Also available: the talk

E. Goldberg. Verification of partial quantifier elimination, arXiv:2303.14928 [cs.LO]

E. Goldberg. Partial quantifier elimination and property generation, arXiv:2303.13811 [cs.LO]

2020

E. Goldberg. On verifying designs with incomplete specification, arXiv:2004.09503 [cs.LO]

E. Goldberg. Generation of a complete set of properties, arXiv:2004.05853 [cs.LO]

E. Goldberg. Partial quantifier elimination by certificate clauses, arXiv:2003.09667 [cs.LO]

2019

E. Goldberg. Partial quantifier elimination with learning, arXiv:1906.10357 [cs.LO]

2018

E. Goldberg, M. Gudemann, D. Kroening, R. Mukherjee. Efficient verification of multi-property designs (The benefit of wrong assumptions), DATE 2018, pp. 43-48,
Also available: the slides of DATE-18 talk , BEST PAPER AWARD

E. Goldberg. Complete test sets and their approximations, FMCAD-2018, pp. 31-38 Also available: the slides of FMCAD-18 talk

E. Goldberg. Improving convergence rate of IC3, arXiv:1809.00503 [cs.LO]

E. Goldberg. Complete test sets and their approximations, arXiv:1808.05750 [cs.LO]

E. Goldberg. Generation of complete test sets, arXiv:1804.00073 [cs.LO]

E. Goldberg. Quantifier elimination with structural learning, arXiv:1810.00160 [cs.LO]

2017

E. Goldberg, M. Gudemann, D. Kroening, R. Mukherjee. Efficient verification of multi-property designs (the benefit of wrong assumptions), extended version, arXiv:1711.05698 [cs.LO]

2016

E.Goldberg. Property checking by logic relaxation, arXiv:1601.02742 [cs.LO] (A technical report archived at Cornell University Library.)

E.Goldberg. Property checking without invariant generation, arXiv:1602.05829 [cs.LO] (A technical report archived at Cornell University Library.)

E.Goldberg. Equivalence checking by logic relaxation, Proceedings of FMCAD-16, pp. 49-57 Also available: the slides of FMCAD-16 talk

2015

E.Goldberg. Equivalence checking by logic relaxation, arXiv:1511.01368 [cs.LO] (A technical report archived at Cornell University Library.)

E.Goldberg. Equivalence checking and simulation by computing range reduction, arXiv:1507.02297 [cs.LO] (A technical report archived at Cornell University Library.)

2014

E.Goldberg, P.Manolios. Partial quantifier elimination , HVC-14, Israel, LNCS-8855, pp.148-165, 2014 Also available: the slides of HVC-14 talk

E.Goldberg, P.Manolios. Bug hunting by computing range reduction , arXiv:1408.7039 [cs.LO] (A technical report archived at Cornell University Library.)

E.Goldberg, P.Manolios. Software for quantifier elimination in propositional logic, ICMS-14, Seoul, Korea, LNCS 8592, pp. 291–294, 2014

E.Goldberg, P.Manolios. Quantifier elimination by dependency sequents, Formal Methods in System Design: Vol. 45, No. 2, 2014 pp. 111-143

2013

E.Goldberg, P.Manolios. Quantifier Elimination Via Clause Redundancy, FMCAD-13, Portland, OR, USA Also available: the slides of FMCAD-13 talk

E.Goldberg, M.Jain, P.Manolios. Verification of Sequential Circuits by Tests-As-Proofs Paradigm, arXiv:1308.0583 [cs.LO] (A technical report archived at Cornell University Library.)

2012

E.Goldberg, P.Manolios. Quantifier Elimination by Dependency Sequents, FMCAD-12, pp. 34-44, Cambridge, UK Also available: the slides of FMCAD-12 talk

E.Goldberg, P.Manolios. Checking Satisfiability by Dependency Sequents, arXiv:1207.5014 [cs.LO] (A technical report archived at Cornell University Library.)

E.Goldberg, P.Manolios. Quantifier Elimination by Dependency Sequents arXiv:1201.5653v4 [cs.LO] (A technical report archived at Cornell University Library.)

E.Goldberg, P.Manolios. Removal of Quantifiers by Elimination of Boundary Points, arXiv:1204.1746v2 [cs.LO] (A technical report archived at Cornell University Library.)

2010

E.Goldberg, P.Manolios. Boundary Points and Resolution, in Advanced Techniques in Logic Synthesis, Optimizations and Applications, Sunil P. Khatri and Kanupriya Gulati, editors, Springer, 2010, chapter 7, pp. 109-128.

E.Goldberg, P.Manolios. SAT-solving Based on Boundary Point Elimination, HVC-2010, Haifa, Israel, LNCS 6504

E.Goldberg, P.Manolios. Generating High-Quality Tests for Boolean Circuits by Treating Tests as Proof Encoding, TAP-2010, Malaga, Spain, LNCS 6143, pp.101-116 Also available: the slides of TAP-2010 talk and an extended version of this talk given at Intel and IBM.

2009

E.Goldberg. Boundary Point Elimination: A Path to Structure Aware SAT-solvers. A talk at a Dagstuhl seminar. Here is a link to the seminar page. Also available: an abstract

E.Goldberg. Boundary points and resolution, SAT-2009, Swansea,Wales,UK, LNCS 5584, pp.147-160. Also available: slides

2008

E.Goldberg. On bridging simulation and formal verification, VMCAI-2008, San Francisco, USA, LNCS 4905, pp.127-141 Also available: slides

E.Goldberg. A decision-making procedure for resolution-based SAT-solvers, SAT-2008, Guangzhou, China,LNCS 4996,pp. 119-132. Also available: slides

E.Goldberg. A Resolution Based SAT-solver Operating on Complete Assignments. Journal on Satisfiability, Boolean Modeling and Computation, Vol. 5 (2008), pp. 217-242.

2007

E.Goldberg,K.Gulati. On complexity of internal and external equivalence checking, DSD-2007,Lubeck, Germany. Also available: slides

E.Goldberg,K.Gulati,S.Khatri. Toggle Equivalence Preserving (TEP) logic synthesis, DSD-2007,Lubeck, Germany. Also available: slides

E.Goldberg. Escaping Local Minima in Logic Synthesis, IWLS-2007,San Diego 2007. Also available: slides

E.Goldberg. Escaping Local Minima in Logic Synthesis (and some other problems of logic synthesis preserving specification). Technical Report CDNL-TR-2007-0123, January 2007

E.Goldberg. On Bridging Simulation and Formal Verification. Technical Report CDNL-TR-2007-0212, February 2007 Also available: a short version

E.Goldberg. Determinization of resolution by an algorithm operating on complete assignments. Technical Report CDNL-TR-2007-0106, January 2007 
The technical report above replaces  the previous report  on "Determinization of resolution by an algorithm operating on complete assignments". 
The new report contains one more table of results and proves that  the set of points visited by FI is actually a point image of the resolution proof FI builds. 
Note that I use a new definition of the point image that is slightly different from  one used in the SAT-2006 paper and in the previous report mentioned above.
E.Goldberg,Y.Novikov. BerkMin: A fast and robust Sat-solver, Discrete Applied Mathematics 155 (2007) pp. 1549-1561

Although the preamble of the paper above says that it was submitted in 2006, in reality it had been in the pipeline of DAM for three years since 2003. This paper is different from our DATE-2002 submission in that every feature of BerkMin is justified experimentally. So you may still find it interesting. I am not allowed to have this paper accessible through my webpage. But I can send it to you by email.

2006 

 The slides of 3 lectures I gave at the workshop "Algorithms for the SAT-Problem". Humboldt University, Berlin, October 27-29, 2006. 
 First lecture. Gives some introduction to SAT and some basic knowledge about resolution proof system. Describes DP and DPLL procedures.  
 Second lecture.Describes the interiors of modern resolution based SAT-solvers.
 Third lecture. Introduces formulas with short resolution proofs that can not be found efficiently. Describes testing satisfiability by 
                 computing a stable set of points/clusters.


E.Goldberg. Determinization of resolution by an algorithm operating on complete assignments. SAT-2006, LNCS 4121, pp.90-95

E.Goldberg,K.Gulati. On Complexity of External and Internal Equivalence Checking. Technical Report CDNL-TR-2006-0105, January 2006

Powerpoint slides of my SAT-2006 talk (short version).

Powerpoint slides of my SAT-2006 talk (long version with experimental results).

2005

E.Goldberg,K.Gulati. Toggle Equivalence Preserving Logic Synthesis. Technical Report CDNL-TR-2005-0912, September 2005

E.Goldberg. Solving satisfiability problem by computing stable sets of points in clusters. Technical Report CDNL-TR-2005-1001, October 2005

E.Goldberg. Equivalence checking of circuits with parameterized specifications. International Conference on Theory and Applications of Satisfiability Testing, St Andrews, UK, June 19-23,2005, LNCS 3569, pp.107-121

Powerpoint slides of my SAT-2005 talk.

E.Goldberg. On Equivalence Checking and Logic Synthesis of Circuits with a Common Specification. Proceedings of GLSVLSI, Chicago, April 17-19, 2005,pp.102-107

E.Goldberg. Testing Satisfiability of CNF Formulas by Computing a Stable Set of Points. Annals of Mathematics and Artificial Intelligence, 43 (1-4): 65-89, January 2005

2004

E. Goldberg. What Sat-solvers can and cannot do. A chapter in Advanced Formal verification. Kluwer Academic Publishers, edited by Rolf Drechsler, 2004, pp.1-43.

E.Goldberg. On equivalence checking and logic synthesis of circuits with a common specification. Technical Report CDNL-TR-2004-1220, August 2004

E.Goldberg. Equivalence checking of dissimilar circuits II. Technical Report CDNL-TR-2004-0830, August 2004

E.Goldberg. Logic synthesis preserving high-level specification. International Workshop on Logic Synthesis, IWLS-2004.

Powerpoint slides of my IWLS-2004 talk.

2003

E.Goldberg, Y.Novikov. Verification of proofs of unsatisfiability for CNF formulas. Design, Automation and Test in Europe. 2003, March 3-7,pp.886-891.

E.Goldberg, Y.Novikov. How good can a resolution based SAT-solver be? Sixth International Conference on Theory and Applications of Satisfiability Testing, Portofino, May 5-8,2003, Italy, LNCS 2919, pp.37-52.

E.Goldberg, Y. Novikov. Equivalence Checking of Dissimilar Circuits. International Workshop on Logic and Synthesis, May 28-30, 2003, USA.

E.Goldberg, Y.Novikov. On complexity of equivalence checking. Technical Report CDNL-TR-2003-08026, August 2003 .

2002

E.Goldberg, M.Prasad, R.Brayton. Using Problem Symmetry in Search Based Satisfiability Algorithms , DATE-2002, Paris,pp. 134-141, BEST PAPER AWARD.

E.Goldberg, Y.Novikov. BerkMin: a Fast and Robust SAT-Solver. DATE-2002,Paris,pp. 142-149 .

E.Goldberg. Testing Satisfiability of CNF Formulas by Computing a Stable Set of Points. Proceedigns of Conference on Automated Deduction, CADE 2002,pp.161-180 .

E. Goldberg. Proving Unsatisfiability of CNFs locally. Journal of Automated Reasoning. vol 28:417-434, 2002.

2001

E. Goldberg, M.Prasad, R.K.Brayton. Using SAT for combinational equivalence checking. Proceedings of DATE-2001, pp. 114 -121.

Novikov Y., Goldberg E. An efficient learning procedure for multiple implication checks. Proceedings of DATE-2001 pp. 127 -133.

Goldberg E. Proving unsatisfiability of CNFs locally. Proceedings of LICS 2001 Workshop on Theory and Applications of Satisfiability Testing.

2000

E.Goldberg,A.Saldanha. Timing Analysis with Implicitly Specified False Paths. VLSI-2000,pp. 518-522.

A few papers written in the past century :-):-)

L.P.Carloni,E.I.Goldberg,T.Villa,R.K.Brayton and A.L.Sangiovanni-Vincentelli. Aura II: Combining Negative Thinking and Branch-and-Bound in Unate Covering Problems. In "VLSI: Systems on a Chip" (L.M. Silveira, R. Reis, S. Devadas editors), Kluwer 1999.

Goldberg E.I., Kukimoto K., Brayton R.K. Combinational verification based on high-level functional specifications. Proceedings of DATE-98, Paris, p.803-807.

Goldberg, E.I., Villa T., Brayton R.K., Sangiovanni-Vincentelli A.L. A fast and robust exact algorithm for face embedding. Proceedings of IEEE International Conference on Computer Aided Design (ICCAD), San Jose, CA, USA, 9-13 Nov. 1997). Los Alamitos, CA, USA: IEEE Comput. Soc, 1997. p. 296-303.

Goldberg, E.I., Carloni L.P., Villa T., Brayton R.K. Negative thinking by incremental problem solving: application to unate covering. Proceedings of IEEE International Conference on Computer Aided Design (ICCAD), San Jose, CA, USA, 9-13 Nov. 1997). Los Alamitos, CA, USA:IEEE Comput. Soc, 1997. p. 91-99.