Fabio Somenzi

According to our database1, Fabio Somenzi authored at least 162 papers between 1983 and 2019.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

On csauthors.net:

Bibliography

2019
Omega-Regular Objectives in Model-Free Reinforcement Learning.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

Reinforcement Learning and Formal Requirements.
Proceedings of the Numerical Software Verification - 12th International Workshop, 2019

2018
Global Almost-Sure Reachability in Stochastic Constant-Rate Multi-Mode Systems.
Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week), 2018

2017
The Reach-Avoid Problem for Constant-Rate Multi-mode Systems.
Proceedings of the Automated Technology for Verification and Analysis, 2017

2016
Proving Parameterized Systems Safe by Generalizing Clausal Proofs of Small Instances.
Proceedings of the Computer Aided Verification - 28th International Conference, 2016

2014
Statistically Sound Verification and Optimization for Complex Systems.
Proceedings of the Automated Technology for Verification and Analysis, 2014

Sparse statistical model inference for analog circuits under process variations.
Proceedings of the 19th Asia and South Pacific Design Automation Conference, 2014

2013
Using Abstraction to Guide the Search for Long Error Traces.
IEEE Trans. on CAD of Integrated Circuits and Systems, 2013

Safety first: a two-stage algorithm for the synthesis of reactive systems.
STTT, 2013

From statistical model checking to statistical model inference: characterizing the effect of process variations in analog circuits.
Proceedings of the IEEE/ACM International Conference on Computer-Aided Design, 2013

Efficient handling of obligation constraints in synthesis from omega-regular specifications.
Proceedings of the Formal Methods in Computer-Aided Design, 2013

Better generalization in IC3.
Proceedings of the Formal Methods in Computer-Aided Design, 2013

2012
Piecewise linear modeling of nonlinear devices for formal verification of analog circuits.
Proceedings of the Formal Methods in Computer-Aided Design, 2012

Incremental, Inductive CTL Model Checking.
Proceedings of the Computer Aided Verification - 24th International Conference, 2012

2011
IC3: where monolithic and incremental meet.
Proceedings of the International Conference on Formal Methods in Computer-Aided Design, 2011

A Study of Sweeping Algorithms in the Context of Model Checking.
Proceedings of the First International Workshop on Design and Implementation of Formal Tools and Systems, 2011

An incremental approach to model checking progress properties.
Proceedings of the International Conference on Formal Methods in Computer-Aided Design, 2011

Clause simplification through dominator analysis.
Proceedings of the Design, Automation and Test in Europe, 2011

2010
Making Deduction More Effective in SAT Solvers.
IEEE Trans. on CAD of Integrated Circuits and Systems, 2010

2009
Efficient Term-ITE Conversion for Satisfiability Modulo Theories.
Proceedings of the Theory and Applications of Satisfiability Testing, 2009

On-the-Fly Clause Improvement.
Proceedings of the Theory and Applications of Satisfiability Testing, 2009

Safety first: A two-stage algorithm for LTL games.
Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, 2009

Constraints in one-to-many concretization for abstraction refinement.
Proceedings of the 46th Design Automation Conference, 2009

2008
A Hybrid Algorithm for LTL Games.
Proceedings of the Verification, 2008

Improved Visibility in One-to-Many Trace Concretization.
Proceedings of the Design, Automation and Test in Europe, 2008

Application of Formal Word-Level Analysis to Constrained Random Simulation.
Proceedings of the Computer Aided Verification, 20th International Conference, 2008

2007
Disequality Management in Integer Difference Logic via Finite Instantiations.
JSAT, 2007

Preface.
Electr. Notes Theor. Comput. Sci., 2007

Alembic: An Efficient Algorithm for CNF Preprocessing.
Proceedings of the 44th Design Automation Conference, 2007

2006
Abstraction Refinement for Large Scale Model Checking
Series on Integrated Circuits and Systems, Springer, ISBN: 978-0-387-34600-7, 2006

Improving Ariadne's Bundle by Following Multiple Threads in Abstraction Refinement.
IEEE Trans. on CAD of Integrated Circuits and Systems, 2006

Compositional SCC Analysis for Language Emptiness.
Formal Methods in System Design, 2006

Termination Criteria for Bounded Model Checking: Extensions and Comparison.
Electr. Notes Theor. Comput. Sci., 2006

Efficient Abstraction Refinement in Interpolation-Based Unbounded Model Checking.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2006

Decomposing image computation for symbolic reachability analysis using control flow information.
Proceedings of the 2006 International Conference on Computer-Aided Design, 2006

Finite Instantiations for Integer Difference Logic.
Proceedings of the Formal Methods in Computer-Aided Design, 6th International Conference, 2006

Strong conflict analysis for propositional satisfiability.
Proceedings of the Conference on Design, Automation and Test in Europe, 2006

Guiding simulation with increasingly refined abstract traces.
Proceedings of the 43rd Design Automation Conference, 2006

Automatic invariant strengthening to prove properties in bounded model checking.
Proceedings of the 43rd Design Automation Conference, 2006

Logic synthesis and verification algorithms.
Springer, ISBN: 978-0-387-31004-6, 2006

2005
Abstraction refinement in symbolic model checking using satisfiability as the only decision procedure.
STTT, 2005

An Incremental Algorithm to Check Satisfiability for Bounded Model Checking.
Electr. Notes Theor. Comput. Sci., 2005

Efficient Conflict Analysis for Finding All Satisfying Assignments of a Boolean Circuit.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

Prime clauses for fast enumeration of satisfying assignments to boolean circuits.
Proceedings of the 42nd Design Automation Conference, 2005

Automatic Generation of Hints for Symbolic Traversal.
Proceedings of the Correct Hardware Design and Verification Methods, 2005

2004
Minimal Assignments for Bounded Model Checking.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2004

CirCUs: A Hybrid Satisfiability Solver.
Proceedings of the Theory and Applications of Satisfiability Testing, 2004

CirCUs: A Hybrid Satisfiability Solver.
Proceedings of the SAT 2004, 2004

Fine-Grain Abstraction and Sequential Don't Cares for Large Scale Model Checking.
Proceedings of the 22nd IEEE International Conference on Computer Design: VLSI in Computers & Processors (ICCD 2004), 2004

Efficient computation of small abstraction refinements.
Proceedings of the 2004 International Conference on Computer-Aided Design, 2004

Increasing the Robustness of Bounded Model Checking by Computing Lower Bounds on the Reachable States.
Proceedings of the Formal Methods in Computer-Aided Design, 5th International Conference, 2004

Refining the SAT decision ordering for bounded model checking.
Proceedings of the 41th Design Automation Conference, 2004

CirCUs: A Satisfiability Solver Geared towards Bounded Model Checking.
Proceedings of the Computer Aided Verification, 16th International Conference, 2004

Proving More Properties with Bounded Model Checking.
Proceedings of the Computer Aided Verification, 16th International Conference, 2004

2003
A satisfiability-based approach to abstraction refinement in model checking.
Electr. Notes Theor. Comput. Sci., 2003

Improving Ariadneýs Bundle by Following Multiple Threads in Abstraction Refinement.
Proceedings of the 2003 International Conference on Computer-Aided Design, 2003

The Compositional Far Side of Image Computation.
Proceedings of the 2003 International Conference on Computer-Aided Design, 2003

Dos and don'ts of CTL state coverage estimation.
Proceedings of the 40th Design Automation Conference, 2003

Formal verification - prove it or pitch it.
Proceedings of the 40th Design Automation Conference, 2003

The Charme of Abstract Entities.
Proceedings of the Correct Hardware Design and Verification Methods, 2003

On Complementing Nondeterministic Büchi Automata.
Proceedings of the Correct Hardware Design and Verification Methods, 2003

2002
Fate and Free Will in Error Traces.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2002

Fine-Grain Conjunction Scheduling for Symbolic Reachability Analysis.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2002

Analysis of Symbolic SCC Hull Algorithms.
Proceedings of the Formal Methods in Computer-Aided Design, 4th International Conference, 2002

Vacuum Cleaning CTL Formulae.
Proceedings of the Computer Aided Verification, 14th International Conference, 2002

Fair Simulation Minimization.
Proceedings of the Computer Aided Verification, 14th International Conference, 2002

2001
Using lower bounds during dynamic BDD minimization.
IEEE Trans. on CAD of Integrated Circuits and Systems, 2001

Efficient manipulation of decision diagrams.
STTT, 2001

Divide and Compose: SCC Refinement for Language Emptiness.
Proceedings of the CONCUR 2001, 2001

2000
Linear sifting of decision diagrams and its application insynthesis.
IEEE Trans. on CAD of Integrated Circuits and Systems, 2000

Fundamental CAD algorithms.
IEEE Trans. on CAD of Integrated Circuits and Systems, 2000

A Comparative Study of Symbolic Algorithms for the Computation of Fair Cycles.
Proceedings of the Formal Methods in Computer-Aided Design, Third International Conference, 2000

Border-Block Triangular Form and Conjunction Schedule in Image Computation.
Proceedings of the Formal Methods in Computer-Aided Design, Third International Conference, 2000

An Algorithm for Strongly Connected Component Analysis in n log n Symbolic Steps.
Proceedings of the Formal Methods in Computer-Aided Design, Third International Conference, 2000

Power and Delay Reduction via Simultaneous Logic and Placement Optimization in FPGAs.
Proceedings of the 2000 Design, 2000

To split or to conjoin: the question in image computation.
Proceedings of the 37th Conference on Design Automation, 2000

Optimizing sequential verification by retiming transformations.
Proceedings of the 37th Conference on Design Automation, 2000

Symbolic guided search for CTL model checking.
Proceedings of the 37th Conference on Design Automation, 2000

Efficient Büchi Automata from LTL Formulae.
Proceedings of the Computer Aided Verification, 12th International Conference, 2000

1999
Symbolic State Exploration.
Electr. Notes Theor. Comput. Sci., 1999

Efficient Fixpoint Computation for Invariant Checking.
Proceedings of the IEEE International Conference On Computer Design, 1999

Least fixpoint approximations for reachability analysis.
Proceedings of the 1999 IEEE/ACM International Conference on Computer-Aided Design, 1999

Lazy group sifting for efficient symbolic state traversal of FSMs.
Proceedings of the 1999 IEEE/ACM International Conference on Computer-Aided Design, 1999

Using Combinational Verification for Sequential Circuits.
Proceedings of the 1999 Design, 1999

Hints to accelerate Symbolic Traversal.
Proceedings of the Correct Hardware Design and Verification Methods, 1999

Efficient Decision Procedures for Model Checking of Linear Time Logic Properties.
Proceedings of the Computer Aided Verification, 11th International Conference, 1999

1998
On the optimization power of retiming and resynthesis transformations.
Proceedings of the 1998 IEEE/ACM International Conference on Computer-Aided Design, 1998

Approximate reachability don't cares for CTL model checking.
Proceedings of the 1998 IEEE/ACM International Conference on Computer-Aided Design, 1998

Symbolic algorithms for layout-oriented synthesis of pass transistor logic circuits.
Proceedings of the 1998 IEEE/ACM International Conference on Computer-Aided Design, 1998

A Performance Study of BDD-Based Model Checking.
Proceedings of the Formal Methods in Computer-Aided Design, 1998

Approximation and Decomposition of Binary Decision Diagrams.
Proceedings of the 35th Conference on Design Automation, 1998

In-Place Power Optimization for LUT-Based FPGAs.
Proceedings of the 35th Conference on Design Automation, 1998

Function Decomposition and Synthesis Using Linear Sifting.
Proceedings of the ASP-DAC '98, 1998

1997
Function Decomposition and Synthesis Using Linear Sifting
Universität Trier, Mathematik/Informatik, Forschungsbericht, 1997

Formal verification of digital systems by automatic reduction of data paths.
IEEE Trans. on CAD of Integrated Circuits and Systems, 1997

Symbolic timing analysis and resynthesis for low power of combinational circuits containing false paths.
IEEE Trans. on CAD of Integrated Circuits and Systems, 1997

Arithmetic Boolean Expression Manipulator Using BDDs.
Formal Methods in System Design, 1997

A Symbolic Algorithms for Maximum Flow in 0-1 Networks.
Formal Methods in System Design, 1997

A symbolic algorithm for low-power sequential synthesis.
Proceedings of the 1997 International Symposium on Low Power Electronics and Design, 1997

Linear Sifting of Decision Diagrams.
Proceedings of the 34st Conference on Design Automation, 1997

Remembrance of Things Past: Locality and Memory in BDDs.
Proceedings of the 34st Conference on Design Automation, 1997

High-Level Power Modeling, Estimation, and Optimization.
Proceedings of the 34st Conference on Design Automation, 1997

1996
Linear Sifting of Decision Diagrams
Universität Trier, Mathematik/Informatik, Forschungsbericht, 1996

Markovian analysis of large finite state machines.
IEEE Trans. on CAD of Integrated Circuits and Systems, 1996

Algorithms for approximate FSM traversal based on state space decomposition.
IEEE Trans. on CAD of Integrated Circuits and Systems, 1996

Automatic state space decomposition for approximate FSM traversal based on circuit analysis.
IEEE Trans. on CAD of Integrated Circuits and Systems, 1996

Symbolic computation of logic implications for technology-dependent low-power synthesis.
Proceedings of the 1996 International Symposium on Low Power Electronics and Design, 1996

Tearing based automatic abstraction for CTL model checking.
Proceedings of the 1996 IEEE/ACM International Conference on Computer-Aided Design, 1996

Modular Verification of Multipliers.
Proceedings of the Formal Methods in Computer-Aided Design, First International Conference, 1996



Logic synthesis and verification algorithms.
Kluwer, ISBN: 978-0-7923-9746-5, 1996

1995
CMOS dynamic power estimation based on collapsible current source transistor modeling.
Proceedings of the 1995 International Symposium on Low Power Design 1995, 1995

High-density reachability analysis.
Proceedings of the 1995 IEEE/ACM International Conference on Computer-Aided Design, 1995

Who are the variables in your neighborhood.
Proceedings of the 1995 IEEE/ACM International Conference on Computer-Aided Design, 1995

Boolean techniques for low power driven re-synthesis.
Proceedings of the 1995 IEEE/ACM International Conference on Computer-Aided Design, 1995

Computing the Maximum Power Cycles of a Sequential Circuit.
Proceedings of the 32st Conference on Design Automation, 1995

1994
Don't care sequences and the optimization of interacting finite state machines.
IEEE Trans. on CAD of Integrated Circuits and Systems, 1994

Exact and heuristic algorithms for the minimization of incompletely specified state machines.
IEEE Trans. on CAD of Integrated Circuits and Systems, 1994

Extended BDDs: Trading off Canonicity for Structure in Verification Algorithms.
Formal Methods in System Design, 1994

A Structural Approach to State Space Decomposition for Approximate Reachability Analysis.
Proceedings of the Proceedings 1994 IEEE International Conference on Computer Design: VLSI in Computer & Processors, 1994

Symmetry detection and dynamic variable ordering of decision diagrams.
Proceedings of the 1994 IEEE/ACM International Conference on Computer-Aided Design, 1994

Re-encoding sequential circuits to reduce power dissipation.
Proceedings of the 1994 IEEE/ACM International Conference on Computer-Aided Design, 1994

A symbolic method to reduce power consumption of circuits containing false paths.
Proceedings of the 1994 IEEE/ACM International Conference on Computer-Aided Design, 1994

An ADD-based algorithm for shortest path back-tracing of large graphs.
Proceedings of the Fourth Great Lakes Symposium on Design Automation of High Performance VLSI Systems, 1994

Symbolic Algorithms to Calculate Steady-State Probabilities of a Finite State Machine.
Proceedings of the EDAC - The European Conference on Design Automation, ETC - European Test Conference, EUROASIC - The European Event in ASIC Design, Proceedings, February 28, 1994

A State Space Decomposition Algorithm for Approximate FSM Traversal.
Proceedings of the EDAC - The European Conference on Design Automation, ETC - European Test Conference, EUROASIC - The European Event in ASIC Design, Proceedings, February 28, 1994

Timing Analysis of Combinational Circuits using ADD's.
Proceedings of the EDAC - The European Conference on Design Automation, ETC - European Test Conference, EUROASIC - The European Event in ASIC Design, Proceedings, February 28, 1994

Probabilistic Analysis of Large Finite State Machines.
Proceedings of the 31st Conference on Design Automation, 1994

1993
Redundancy identification/removal and test generation for sequential circuits using implicit state enumeration.
IEEE Trans. on CAD of Integrated Circuits and Systems, 1993

Synchronizing sequences and symbolic traversal techniques in test generation.
J. Electronic Testing, 1993

A symbolic algorithm for maximum flow in 0-1 networks.
Proceedings of the 1993 IEEE/ACM International Conference on Computer-Aided Design, 1993

Algebraic decision diagrams and their applications.
Proceedings of the 1993 IEEE/ACM International Conference on Computer-Aided Design, 1993

Minimum Length Synchronizing Sequences of Finite State Machine.
Proceedings of the 30th Design Automation Conference. Dallas, 1993

Algorithms for Approximate FSM Traversal.
Proceedings of the 30th Design Automation Conference. Dallas, 1993

Automatic Generation of Network Invariants for the Verification of Iterative Sequential Systems.
Proceedings of the Computer Aided Verification, 5th International Conference, 1993

1992
The Role of Prime Compatibles in the Minimization of Finite State Machines.
Proceedings of the Proceedings 1992 IEEE International Conference on Computer Design: VLSI in Computer & Processors, 1992

Verification of systems containing counters.
Proceedings of the 1992 IEEE/ACM International Conference on Computer-Aided Design, 1992

A new algorithm for the binate covering problem and its application to the minimization of Boolean relations.
Proceedings of the 1992 IEEE/ACM International Conference on Computer-Aided Design, 1992

Inductive Verification of Iterative Systems.
Proceedings of the 29th Design Automation Conference, 1992

1991
Fault simulation for general FCMOS ICs.
J. Electronic Testing, 1991

Fast Sequential ATPG Based on Implicit State Enumeration.
Proceedings of the Proceedings IEEE International Test Conference 1991, 1991

Redundancy Identification and Removal Based on Implicit State Enumeration.
Proceedings of the Proceedings 1991 IEEE International Conference on Computer Design: VLSI in Computer & Processors, 1991

Don't Care Sequences and the Optimization of Interacting Finite State Machines.
Proceedings of the 1991 IEEE/ACM International Conference on Computer-Aided Design, 1991

Variable Ordering and Selection for FSM Traversal.
Proceedings of the 1991 IEEE/ACM International Conference on Computer-Aided Design, 1991

Extended BDD's: Trading off Canonicity for Structure in Verification Algorithms.
Proceedings of the 1991 IEEE/ACM International Conference on Computer-Aided Design, 1991

Periodic signal suppression in a concurrent fault simulator.
Proceedings of the conference on European design automation, 1991

Exact and heuristic algorithms for the minimization of incompletely specified state machines.
Proceedings of the conference on European design automation, 1991

1990
Minimization of Symbolic Relations.
Proceedings of the IEEE/ACM International Conference on Computer-Aided Design, 1990

ATPG Aspects of FSM Verification.
Proceedings of the IEEE/ACM International Conference on Computer-Aided Design, 1990

An iterative algorithm for the binate covering problem.
Proceedings of the European Design Automation Conference, 1990

Results on the Interface between Formal Verification and ATPG.
Proceedings of the Computer-Aided Verification, 1990

1989
An exact minimizer for Boolean relations.
Proceedings of the 1989 IEEE International Conference on Computer-Aided Design, 1989

1988
MOZART: a concurrent multilevel simulator.
IEEE Trans. on CAD of Integrated Circuits and Systems, 1988

Don't cares and global flow analysis of Boolean networks.
Proceedings of the 1988 IEEE International Conference on Computer-Aided Design, 1988

Fault simulation in a multilevel environment: the MOZART approach.
Proceedings of the Eighteenth International Symposium on Fault-Tolerant Computing, 1988

The Performance of the Concurrent Fault Simulation Algorithms in MOZART.
Proceedings of the 25th ACM/IEEE Conference on Design Automation, 1988

1987
Advances in Concurrent Multilevel Simulation.
IEEE Trans. on CAD of Integrated Circuits and Systems, 1987

Fast and Coherent Simulation with Zero Delay Elements.
IEEE Trans. on CAD of Integrated Circuits and Systems, 1987

1985
Testing Strategy and Technique for Macro-Based Circuits.
IEEE Trans. Computers, 1985

1984
PART: Programmable Array Testing Based on a Partitioning Algorithm.
IEEE Trans. on CAD of Integrated Circuits and Systems, 1984

1983
A new integrated system for PLA testing and verification.
Proceedings of the 20th Design Automation Conference, 1983


  Loading...