Fabio Somenzi

Orcid: 0000-0002-2085-2003

According to our database1, Fabio Somenzi authored at least 184 papers between 1983 and 2024.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
A PAC Learning Algorithm for LTL and Omega-Regular Objectives in MDPs.
Proceedings of the Thirty-Eighth AAAI Conference on Artificial Intelligence, 2024

Assume-Guarantee Reinforcement Learning.
Proceedings of the Thirty-Eighth AAAI Conference on Artificial Intelligence, 2024

Omega-Regular Decision Processes.
Proceedings of the Thirty-Eighth AAAI Conference on Artificial Intelligence, 2024

2023
Multi-objective ω-Regular Reinforcement Learning.
Formal Aspects Comput., June, 2023

Mungojerrie: Linear-Time Objectives in Model-Free Reinforcement Learning.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2023

Omega-Regular Reward Machines.
Proceedings of the ECAI 2023 - 26th European Conference on Artificial Intelligence, September 30 - October 4, 2023, Kraków, Poland, 2023

Policy Synthesis and Reinforcement Learning for Discounted LTL.
Proceedings of the Computer Aided Verification - 35th International Conference, 2023

2022
Compositional Reinforcement Learning for Discrete-Time Stochastic Control Systems.
CoRR, 2022

Alternating Good-for-MDP Automata.
CoRR, 2022

Recursive Reinforcement Learning.
Proceedings of the Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, 2022

Reinforcement Learning with Guarantees that Hold for Ever.
Proceedings of the Formal Methods for Industrial Critical Systems, 2022

Alternating Good-for-MDPs Automata.
Proceedings of the Automated Technology for Verification and Analysis, 2022

An Impossibility Result in Automata-Theoretic Reinforcement Learning.
Proceedings of the Automated Technology for Verification and Analysis, 2022

Translating Omega-Regular Specifications to Average Objectives for Model-Free Reinforcement Learning.
Proceedings of the 21st International Conference on Autonomous Agents and Multiagent Systems, 2022

2021
Mungojerrie: Reinforcement Learning of Linear-Time Objectives.
CoRR, 2021

Model-Free Reinforcement Learning for Lexicographic Omega-Regular Objectives.
Proceedings of the Formal Methods - 24th International Symposium, 2021

Model-Free Reinforcement Learning for Branching Markov Decision Processes.
Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

2020
Reward Shaping for Reinforcement Learning with Omega-Regular Objectives.
CoRR, 2020

Good-for-MDPs Automata for Probabilistic Analysis and Reinforcement Learning.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2020

Formal Controller Synthesis for Continuous-Space MDPs via Model-Free Reinforcement Learning.
Proceedings of the 11th ACM/IEEE International Conference on Cyber-Physical Systems, 2020

Model-Free Reinforcement Learning for Stochastic Parity Games.
Proceedings of the 31st International Conference on Concurrency Theory, 2020

Faithful and Effective Reward Schemes for Model-Free Reinforcement Learning of Omega-Regular Objectives.
Proceedings of the Automated Technology for Verification and Analysis, 2020

2019
Good-for-MDPs Automata.
CoRR, 2019

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

Limit reachability for model-free reinforcement learning of ω-regular objectives.
Proceedings of the Fifth International Workshop on Symbolic-Numeric methods for Reasoning about CPS and IoT, 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. Comput. Aided Des. Integr. Circuits Syst., 2013

Safety first: a two-stage algorithm for the synthesis of reactive systems.
Int. J. Softw. Tools Technol. Transf., 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. Comput. Aided Des. Integr. Circuits Syst., 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.
J. Satisf. Boolean Model. Comput., 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. Comput. Aided Des. Integr. Circuits Syst., 2006

Compositional SCC Analysis for Language Emptiness.
Formal Methods Syst. Des., 2006

An Algorithm for Strongly Connected Component Analysis in <i>n</i> log <i>n</i> Symbolic Steps.
Formal Methods Syst. Des., 2006

Preface.
Proceedings of the Workshop on Verification and Debugging, 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.
Int. J. Softw. Tools Technol. Transf., 2005

Termination Criteria for Bounded Model Checking: Extensions and Comparison.
Proceedings of the Third International Workshop on Bounded Model Checking, 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
Fate and free will in error traces.
Int. J. Softw. Tools Technol. Transf., 2004

An Incremental Algorithm to Check Satisfiability for Bounded Model Checking.
Proceedings of the 2nd International Workshop on Bounded Model Checking, 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

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.
Proceedings of the First International Workshop on Bounded Model Checking, 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
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. Comput. Aided Des. Integr. Circuits Syst., 2001

Efficient manipulation of decision diagrams.
Int. J. Softw. Tools Technol. Transf., 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. Comput. Aided Des. Integr. Circuits Syst., 2000

Fundamental CAD algorithms.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 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

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.
Proceedings of the First International Workshop on Symbolic Model Checking, 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
High-level power modeling, estimation, and optimization.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 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

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. Comput. Aided Des. Integr. Circuits Syst., 1997

Symbolic timing analysis and resynthesis for low power of combinational circuits containing false paths.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1997

Arithmetic Boolean Expression Manipulator Using BDDs.
Formal Methods Syst. Des., 1997

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

Algebraic Decision Diagrams and Their Applications.
Formal Methods Syst. Des., 1997

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

Remembrance of Things Past: Locality and Memory in BDDs.
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. Comput. Aided Des. Integr. Circuits Syst., 1996

Algorithms for approximate FSM traversal based on state space decomposition.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1996

Automatic state space decomposition for approximate FSM traversal based on circuit analysis.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 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. Comput. Aided Des. Integr. Circuits Syst., 1994

Exact and heuristic algorithms for the minimization of incompletely specified state machines.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1994

Extended BDDs: Trading off Canonicity for Structure in Verification Algorithms.
Formal Methods Syst. Des., 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. Comput. Aided Des. Integr. Circuits Syst., 1993

Synchronizing sequences and symbolic traversal techniques in test generation.
J. Electron. Test., 1993

A symbolic algorithm for maximum flow in 0-1 networks.
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. Electron. Test., 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

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
MSYN: Automatic synthesis of hardware.
Microprocessing and Microprogramming, 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. Comput. Aided Des. Integr. Circuits Syst., 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. Comput. Aided Des. Integr. Circuits Syst., 1987

Fast and Coherent Simulation with Zero Delay Elements.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1987

1986
Fault detection in programmable logic arrays.
Proc. IEEE, 1986

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. Comput. Aided Des. Integr. Circuits Syst., 1984

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


  Loading...