| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | HyoJung Han, HoonSang Jin, Fabio Somenzi |
Clause simplification through dominator analysis.  |
DATE  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | HyoJung Han, Fabio Somenzi, HoonSang Jin |
Making Deduction More Effective in SAT Solvers. |
IEEE Trans. on CAD of Integrated Circuits and Systems |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Saqib Sohail, Fabio Somenzi |
Safety first: A two-stage algorithm for LTL games. |
FMCAD |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | HyoJung Han, Fabio Somenzi |
On-the-Fly Clause Improvement. |
SAT |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Hyondeuk Kim, Fabio Somenzi, HoonSang Jin |
Efficient Term-ITE Conversion for Satisfiability Modulo Theories. |
SAT |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Kuntal Nanshi, Fabio Somenzi |
Constraints in one-to-many concretization for abstraction refinement. |
DAC |
2009 |
DBLP DOI BibTeX RDF |
simulation, model checking, abstraction refinement |
| 1 | Kuntal Nanshi, Fabio Somenzi |
Improved Visibility in One-to-Many Trace Concretization. |
DATE |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Hyondeuk Kim, HoonSang Jin, Kavita Ravi, Petr Spacek, John Pierce, Robert P. Kurshan, Fabio Somenzi |
Application of Formal Word-Level Analysis to Constrained Random Simulation. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Saqib Sohail, Fabio Somenzi, Kavita Ravi |
A Hybrid Algorithm for LTL Games. |
VMCAI |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Hyondeuk Kim, HoonSang Jin, Fabio Somenzi |
Disequality Management in Integer Difference Logic via Finite Instantiations. |
JSAT |
2007 |
DBLP BibTeX RDF |
|
| 1 | Roderick Bloem, Marco Roveri, Fabio Somenzi |
Preface. |
Electr. Notes Theor. Comput. Sci. |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | HyoJung Han, Fabio Somenzi |
Alembic: An Efficient Algorithm for CNF Preprocessing. |
DAC |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Mohammad Awedh, Fabio Somenzi |
Termination Criteria for Bounded Model Checking: Extensions and Comparison. |
Electr. Notes Theor. Comput. Sci. |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Chao Wang, Bing Li, HoonSang Jin, Gary D. Hachtel, Fabio Somenzi |
Improving Ariadne's Bundle by Following Multiple Threads in Abstraction Refinement. |
IEEE Trans. on CAD of Integrated Circuits and Systems |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Roderick Bloem, Harold N. Gabow, Fabio Somenzi |
An Algorithm for Strongly Connected Component Analysis in n log n Symbolic Steps. |
Formal Methods in System Design |
2006 |
DBLP DOI BibTeX RDF |
language emptiness, Büchi automata, Streett automata, model checking, binary decision diagrams, depth-first search, breadth-first search, strongly connected components, symbolic algorithms |
| 1 | Chao Wang, Roderick Bloem, Gary D. Hachtel, Kavita Ravi, Fabio Somenzi |
Compositional SCC Analysis for Language Emptiness. |
Formal Methods in System Design |
2006 |
DBLP DOI BibTeX RDF |
language emptiness, model checking, BDD, LTL, abstraction refinement |
| 1 | Gary D. Hachtel, Fabio Somenzi |
Logic synthesis and verification algorithms. |
|
2006 |
DOI RDF |
|
| 1 | Bing Li, Fabio Somenzi |
Efficient Abstraction Refinement in Interpolation-Based Unbounded Model Checking. |
TACAS |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Hyondeuk Kim, Fabio Somenzi |
Finite Instantiations for Integer Difference Logic. |
FMCAD |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Mohammad Awedh, Fabio Somenzi |
Automatic invariant strengthening to prove properties in bounded model checking. |
DAC |
2006 |
DBLP DOI BibTeX RDF |
SAT, bounded model checking |
| 1 | Kuntal Nanshi, Fabio Somenzi |
Guiding simulation with increasingly refined abstract traces. |
DAC |
2006 |
DBLP DOI BibTeX RDF |
simulation, model checking, abstraction refinement |
| 1 | HoonSang Jin, Fabio Somenzi |
Strong conflict analysis for propositional satisfiability. |
DATE |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | David Ward, Fabio Somenzi |
Decomposing image computation for symbolic reachability analysis using control flow information. |
ICCAD |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | HoonSang Jin, Fabio Somenzi |
An Incremental Algorithm to Check Satisfiability for Bounded Model Checking. |
Electr. Notes Theor. Comput. Sci. |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Bing Li, Chao Wang, Fabio Somenzi |
Abstraction refinement in symbolic model checking using satisfiability as the only decision procedure. |
STTT |
2005 |
DBLP DOI BibTeX RDF |
Unsatisfiability proof, Bounded model checking, Satisfiability problem, Abstraction refinement |
| 1 | HoonSang Jin, HyoJung Han, Fabio Somenzi |
Efficient Conflict Analysis for Finding All Satisfying Assignments of a Boolean Circuit. |
TACAS |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | HoonSang Jin, Fabio Somenzi |
Prime clauses for fast enumeration of satisfying assignments to boolean circuits. |
DAC |
2005 |
DBLP DOI BibTeX RDF |
AllSAT, minimal satisfying assignment, SAT, CNF |
| 1 | David Ward, Fabio Somenzi |
Automatic Generation of Hints for Symbolic Traversal. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | HoonSang Jin, Kavita Ravi, Fabio Somenzi |
Fate and free will in error traces. |
STTT |
2004 |
DBLP DOI BibTeX RDF |
Reachability game, Model checking, Counterexample |
| 1 | Kavita Ravi, Fabio Somenzi |
Minimal Assignments for Bounded Model Checking. |
TACAS |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Mohammad Awedh, Fabio Somenzi |
Increasing the Robustness of Bounded Model Checking by Computing Lower Bounds on the Reachable States. |
FMCAD |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | HoonSang Jin, Fabio Somenzi |
CirCUs: A Hybrid Satisfiability Solver. |
SAT (Selected Papers |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | HoonSang Jin, Fabio Somenzi |
CirCUs: A Hybrid Satisfiability Solver. |
SAT |
2004 |
DBLP BibTeX RDF |
|
| 1 | Chao Wang, HoonSang Jin, Gary D. Hachtel, Fabio Somenzi |
Refining the SAT decision ordering for bounded model checking. |
DAC |
2004 |
DBLP DOI BibTeX RDF |
decision heuristic, SAT, bounded model checking |
| 1 | HoonSang Jin, Mohammad Awedh, Fabio Somenzi |
CirCUs: A Satisfiability Solver Geared towards Bounded Model Checking. |
CAV |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Mohammad Awedh, Fabio Somenzi |
Proving More Properties with Bounded Model Checking. |
CAV |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Bing Li, Fabio Somenzi |
Efficient computation of small abstraction refinements. |
ICCAD |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Chao Wang, Gary D. Hachtel, Fabio Somenzi |
Fine-Grain Abstraction and Sequential Don't Cares for Large Scale Model Checking. |
ICCD |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Bing Li, Chao Wang, Fabio Somenzi |
A satisfiability-based approach to abstraction refinement in model checking. |
Electr. Notes Theor. Comput. Sci. |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Nikhil Jayakumar, Mitra Purandare, Fabio Somenzi |
Dos and don'ts of CTL state coverage estimation. |
DAC |
2003 |
DBLP DOI BibTeX RDF |
vacuity detection, model checking, state coverage |
| 1 | Rajesh K. Gupta, Shishpal Rawat, Sandeep K. Shukla, Brian Bailey, Daniel K. Beece, Masahiro Fujita, Carl Pixley, John O'Leary, Fabio Somenzi |
Formal verification - prove it or pitch it. |
DAC |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Fabio Somenzi |
The Charme of Abstract Entities. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Sankar Gurumurthy, Orna Kupferman, Fabio Somenzi, Moshe Y. Vardi |
On Complementing Nondeterministic Büchi Automata. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Warren A. Hunt Jr., Fabio Somenzi (eds.) |
Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings |
CAV |
2003 |
DBLP BibTeX RDF |
|
| 1 | Chao Wang, Gary D. Hachtel, Fabio Somenzi |
The Compositional Far Side of Image Computation. |
ICCAD |
2003 |
DBLP DOI BibTeX RDF |
Model checking, Binary Decision Diagrams, Symbolic, image computation |
| 1 | Chao Wang, Bing Li, HoonSang Jin, Gary D. Hachtel, Fabio Somenzi |
Improving Ariadneýs Bundle by Following Multiple Threads in Abstraction Refinement. |
ICCAD |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | HoonSang Jin, Kavita Ravi, Fabio Somenzi |
Fate and Free Will in Error Traces. |
TACAS |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | HoonSang Jin, Andreas Kuehlmann, Fabio Somenzi |
Fine-Grain Conjunction Scheduling for Symbolic Reachability Analysis. |
TACAS |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Fabio Somenzi, Kavita Ravi, Roderick Bloem |
Analysis of Symbolic SCC Hull Algorithms. |
FMCAD |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Mitra Purandare, Fabio Somenzi |
Vacuum Cleaning CTL Formulae. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Sankar Gurumurthy, Roderick Bloem, Fabio Somenzi |
Fair Simulation Minimization. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Rolf Drechsler, Wolfgang Günther, Fabio Somenzi |
Using lower bounds during dynamic BDD minimization. |
IEEE Trans. on CAD of Integrated Circuits and Systems |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Fabio Somenzi |
Efficient manipulation of decision diagrams. |
STTT |
2001 |
DBLP DOI BibTeX RDF |
Strong canonical form, Variable reordering, Binary decision diagrams |
| 1 | Chao Wang, Roderick Bloem, Gary D. Hachtel, Kavita Ravi, Fabio Somenzi |
Divide and Compose: SCC Refinement for Language Emptiness. |
CONCUR |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Melvin A. Breuer, Majid Sarrafzadeh, Fabio Somenzi |
Fundamental CAD algorithms. |
IEEE Trans. on CAD of Integrated Circuits and Systems |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Christoph Meinel, Fabio Somenzi, Thorsten Theobald |
Linear sifting of decision diagrams and its application insynthesis. |
IEEE Trans. on CAD of Integrated Circuits and Systems |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | In-Ho Moon, Gary D. Hachtel, Fabio Somenzi |
Border-Block Triangular Form and Conjunction Schedule in Image Computation. |
FMCAD |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Kavita Ravi, Roderick Bloem, Fabio Somenzi |
A Comparative Study of Symbolic Algorithms for the Computation of Fair Cycles. |
FMCAD |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Roderick Bloem, Harold N. Gabow, Fabio Somenzi |
An Algorithm for Strongly Connected Component Analysis in n log n Symbolic Steps. |
FMCAD |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Gianpiero Cabodi, Stefano Quer, Fabio Somenzi |
Optimizing sequential verification by retiming transformations. |
DAC |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Roderick Bloem, Kavita Ravi, Fabio Somenzi |
Symbolic guided search for CTL model checking. |
DAC |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | In-Ho Moon, James H. Kukula, Kavita Ravi, Fabio Somenzi |
To split or to conjoin: the question in image computation. |
DAC |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Balakrishna Kumthekar, Fabio Somenzi |
Power and Delay Reduction via Simultaneous Logic and Placement Optimization in FPGAs. |
DATE |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Fabio Somenzi, Roderick Bloem |
Efficient Büchi Automata from LTL Formulae. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Fabio Somenzi |
Symbolic State Exploration. |
Electr. Notes Theor. Comput. Sci. |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Kavita Ravi, Fabio Somenzi |
Hints to accelerate Symbolic Traversal. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev K. Ranjan, Vigyan Singhal, Fabio Somenzi, Robert K. Brayton |
Using Combinational Verification for Sequential Circuits. |
DATE |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Roderick Bloem, Kavita Ravi, Fabio Somenzi |
Efficient Decision Procedures for Model Checking of Linear Time Logic Properties. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Hiroyuki Higuchi, Fabio Somenzi |
Lazy group sifting for efficient symbolic state traversal of FSMs. |
ICCAD |
1999 |
DBLP BibTeX RDF |
|
| 1 | In-Ho Moon, James H. Kukula, Thomas R. Shiple, Fabio Somenzi |
Least fixpoint approximations for reachability analysis. |
ICCAD |
1999 |
DBLP BibTeX RDF |
|
| 1 | Kavita Ravi, Fabio Somenzi |
Efficient Fixpoint Computation for Invariant Checking. |
ICCD |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Enrico Macii, Massoud Pedram, Fabio Somenzi |
High-level power modeling, estimation, and optimization. |
IEEE Trans. on CAD of Integrated Circuits and Systems |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Bwolen Yang, Randal E. Bryant, David R. O'Hallaron, Armin Biere, Olivier Coudert, Geert Janssen, Rajeev K. Ranjan, Fabio Somenzi |
A Performance Study of BDD-Based Model Checking. |
FMCAD |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Balakrishna Kumthekar, Luca Benini, Enrico Macii, Fabio Somenzi |
In-Place Power Optimization for LUT-Based FPGAs. |
DAC |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Kavita Ravi, Kenneth L. McMillan, Thomas R. Shiple, Fabio Somenzi |
Approximation and Decomposition of Binary Decision Diagrams. |
DAC |
1998 |
DBLP DOI BibTeX RDF |
transceiver, spread spectrum communication, RF CMOS, digital radio, ISM frequency band |
| 1 | Christoph Meinel, Fabio Somenzi, Thorsten Theobald |
Function Decomposition and Synthesis Using Linear Sifting. |
ASP-DAC |
1998 |
DBLP BibTeX RDF |
|
| 1 | In-Ho Moon, Jae-Young Jang, Gary D. Hachtel, Fabio Somenzi, Jun Yuan, Carl Pixley |
Approximate reachability don't cares for CTL model checking. |
ICCAD |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev K. Ranjan, Vigyan Singhal, Fabio Somenzi, Robert K. Brayton |
On the optimization power of retiming and resynthesis transformations. |
ICCAD |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Fabrizio Ferrandi, Alberto Macii, Enrico Macii, Massimo Poncino, Riccardo Scarsi, Fabio Somenzi |
Symbolic algorithms for layout-oriented synthesis of pass transistor logic circuits. |
ICCAD |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Christoph Meinel, Fabio Somenzi, Thorsten Theobald |
Function Decomposition and Synthesis Using Linear Sifting |
Universität Trier, Mathematik/Informatik, Forschungsbericht |
1997 |
RDF |
|
| 1 | Enrico Macii, Bernard Plessier, Fabio Somenzi |
Formal verification of digital systems by automatic reduction of data paths. |
IEEE Trans. on CAD of Integrated Circuits and Systems |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | R. Iris Bahar, Hyunwoo Cho, Gary D. Hachtel, Enrico Macii, Fabio Somenzi |
Symbolic timing analysis and resynthesis for low power of combinational circuits containing false paths. |
IEEE Trans. on CAD of Integrated Circuits and Systems |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Gary D. Hachtel, Fabio Somenzi |
A Symbolic Algorithms for Maximum Flow in 0-1 Networks. |
Formal Methods in System Design |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Shin-ichi Minato, Fabio Somenzi |
Arithmetic Boolean Expression Manipulator Using BDDs. |
Formal Methods in System Design |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | R. Iris Bahar, Erica A. Frohm, Charles M. Gaona, Gary D. Hachtel, Enrico Macii, Abelardo Pardo, Fabio Somenzi |
Algebraic Decision Diagrams and Their Applications. |
Formal Methods in System Design |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Balakrishna Kumthekar, In-Ho Moon, Fabio Somenzi |
A symbolic algorithm for low-power sequential synthesis. |
ISLPED |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Srilatha Manne, Dirk Grunwald, Fabio Somenzi |
Remembrance of Things Past: Locality and Memory in BDDs. |
DAC |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Enrico Macii, Massoud Pedram, Fabio Somenzi |
High-Level Power Modeling, Estimation, and Optimization. |
DAC |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Christoph Meinel, Fabio Somenzi, Thorsten Theobald |
Linear Sifting of Decision Diagrams. |
DAC |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Christoph Meinel, Fabio Somenzi, Thorsten Theobald |
Linear Sifting of Decision Diagrams |
Universität Trier, Mathematik/Informatik, Forschungsbericht |
1996 |
RDF |
|
| 1 | Hyunwoo Cho, Gary D. Hachtel, Enrico Macii, Massimo Poncino, Fabio Somenzi |
Automatic state space decomposition for approximate FSM traversal based on circuit analysis. |
IEEE Trans. on CAD of Integrated Circuits and Systems |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | Hyunwoo Cho, Gary D. Hachtel, Enrico Macii, Bernard Plessier, Fabio Somenzi |
Algorithms for approximate FSM traversal based on state space decomposition. |
IEEE Trans. on CAD of Integrated Circuits and Systems |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | Gary D. Hachtel, Enrico Macii, Abelardo Pardo, Fabio Somenzi |
Markovian analysis of large finite state machines. |
IEEE Trans. on CAD of Integrated Circuits and Systems |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | Gary D. Hachtel, Fabio Somenzi |
Logic synthesis and verification algorithms. |
|
1996 |
RDF |
|
| 1 | R. Iris Bahar, M. Burns, Gary D. Hachtel, Enrico Macii, H. Shin, Fabio Somenzi |
Symbolic computation of logic implications for technology-dependent low-power synthesis. |
ISLPED |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | Kavita Ravi, Abelardo Pardo, Gary D. Hachtel, Fabio Somenzi |
Modular Verification of Multipliers. |
FMCAD |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | Robert K. Brayton, Gary D. Hachtel, Alberto L. Sangiovanni-Vincentelli, Fabio Somenzi, Adnan Aziz, Szu-Tsung Cheng, Stephen A. Edwards, Sunil P. Khatri, Yuji Kukimoto, Abelardo Pardo, Shaz Qadeer, Rajeev K. Ranjan, Shaker Sarwary, Thomas R. Shiple, Gitanjali Swamy, Tiziano Villa |
VIS. |
FMCAD |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | Robert K. Brayton, Gary D. Hachtel, Alberto L. Sangiovanni-Vincentelli, Fabio Somenzi, Adnan Aziz, Szu-Tsung Cheng, Stephen A. Edwards, Sunil P. Khatri, Yuji Kukimoto, Abelardo Pardo, Shaz Qadeer, Rajeev K. Ranjan, Shaker Sarwary, Thomas R. Shiple, Gitanjali Swamy, Tiziano Villa |
VIS: A System for Verification and Synthesis. |
CAV |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | Woohyuk Lee, Abelardo Pardo, Jae-Young Jang, Gary D. Hachtel, Fabio Somenzi |
Tearing based automatic abstraction for CTL model checking. |
ICCAD |
1996 |
DBLP DOI BibTeX RDF |
ACTL model checking, CTL model checking, conservative ECTL, lattice set, lower bound approximations, pseudo-optimal shortest path, resolution methods, tearing based automatic abstraction, upper bound approximations, formal verification, reactive system, bipartition |
| 1 | Abelardo Pardo, R. Iris Bahar, Srilatha Manne, Peter Feldmann, Gary D. Hachtel, Fabio Somenzi |
CMOS dynamic power estimation based on collapsible current source transistor modeling. |
ISLPD |
1995 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")