A new integrated system for PLA testing and verification. - Fabio Somenzi; Silvano Gai; Marco Mezzalama; Paolo Prinetto (DAC, 1983)

PART: Programmable Array Testing Based on a Partitioning Algorithm. - Fabio Somenzi; Silvano Gai; Marco Mezzalama; Paolo Prinetto (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1984)

Testing Strategy and Technique for Macro-Based Circuits. - Fabio Somenzi; Silvano Gai; Marco Mezzalama; Paolo Prinetto (IEEE Trans. Computers, 1985)

Fault detection in programmable logic arrays. - Fabio Somenzi; Silvano Gai (Proc. IEEE, 1986)

Fast and Coherent Simulation with Zero Delay Elements. - Silvano Gai; Fabio Somenzi; M. Spalla (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1987)

Advances in Concurrent Multilevel Simulation. - Silvano Gai; Fabio Somenzi; Ernst G. Ulrich (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1987)

The Performance of the Concurrent Fault Simulation Algorithms in MOZART. - Silvano Gai; Pier Luca Montessoro; Fabio Somenzi (DAC, 1988)

Fault simulation in a multilevel environment: the MOZART approach. - Gianpiero Cabodi; Silvano Gai; Marco Mezzalama; Pier Luca Montessoro; Fabio Somenzi (FTCS, 1988)

Don't cares and global flow analysis of Boolean networks. - Robert K. Brayton; Ellen M. Sentovich; Fabio Somenzi (ICCAD, 1988)

MOZART: a concurrent multilevel simulator. - Silvano Gai; Pier Luca Montessoro; Fabio Somenzi (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1988)

An exact minimizer for Boolean relations. - Robert K. Brayton; Fabio Somenzi (ICCAD, 1989)

MSYN: Automatic synthesis of hardware. - I. Causarano; R. Guizzeti; M. Pipponzi; Fabio Somenzi (Microprocessing and Microprogramming, 1989)

Results on the Interface between Formal Verification and ATPG. - Hyunwoo Cho; Gary D. Hachtel; Seh-Woong Jeong; Bernard Plessier; Eric M. Schwarz; Fabio Somenzi (CAV (DIMACS/AMS volume), 1990)

An iterative algorithm for the binate covering problem. - M. Pipponzi; Fabio Somenzi (EURO-DAC, 1990)

ATPG Aspects of FSM Verification. - Hyunwoo Cho; Gary D. Hachtel; Seh-Woong Jeong; Bernard Plessier; Eric M. Schwarz; Fabio Somenzi (ICCAD, 1990)

Minimization of Symbolic Relations. - Bill Lin 001; Fabio Somenzi (ICCAD, 1990)

Periodic signal suppression in a concurrent fault simulator. - Tara Weber; Fabio Somenzi (EURO-DAC, 1991)

Extended BDD's: Trading off Canonicity for Structure in Verification Algorithms. - Seh-Woong Jeong; Bernard Plessier; Gary D. Hachtel; Fabio Somenzi (ICCAD, 1991)

Variable Ordering and Selection for FSM Traversal. - Seon-Woong Jeong; Bernard Plessier; Gary D. Hachtel; Fabio Somenzi (ICCAD, 1991)

Don't Care Sequences and the Optimization of Interacting Finite State Machines. - June-Kyung Rho; Gary D. Hachtel; Fabio Somenzi (ICCAD, 1991)

Redundancy Identification and Removal Based on Implicit State Enumeration. - Hyunwoo Cho; Gary D. Hachtel; Fabio Somenzi (ICCD, 1991)

Fast Sequential ATPG Based on Implicit State Enumeration. - Hyunwoo Cho; Gary D. Hachtel; Fabio Somenzi (ITC, 1991)

Fault simulation for general FCMOS ICs. - Michele Favalli; Piero Olivo; Bruno Riccò; Fabio Somenzi (J. Electron. Test., 1991)

Inductive Verification of Iterative Systems. - June-Kyung Rho; Fabio Somenzi (DAC, 1992)

A new algorithm for the binate covering problem and its application to the minimization of Boolean relations. - Seh-Woong Jeong; Fabio Somenzi (ICCAD, 1992)

Verification of systems containing counters. - Enrico Macii; Bernard Plessier; Fabio Somenzi (ICCAD, 1992)

The Role of Prime Compatibles in the Minimization of Finite State Machines. - June-Kyung Rho; Fabio Somenzi (ICCD, 1992)

Automatic Generation of Network Invariants for the Verification of Iterative Sequential Systems. - June-Kyung Rho; Fabio Somenzi (CAV, 1993)

Algorithms for Approximate FSM Traversal. - Hyunwoo Cho; Gary D. Hachtel; Enrico Macii; Bernard Plessier; Fabio Somenzi (DAC, 1993)

Minimum Length Synchronizing Sequences of Finite State Machine. - June-Kyung Rho; Fabio Somenzi; Carl Pixley (DAC, 1993)

A symbolic algorithm for maximum flow in 0-1 networks. - Gary D. Hachtel; Fabio Somenzi (ICCAD, 1993)

Synchronizing sequences and symbolic traversal techniques in test generation. - Hyunwoo Cho; Seh-Woong Jeong; Fabio Somenzi; Carl Pixley (J. Electron. Test., 1993)

Redundancy identification/removal and test generation for sequential circuits using implicit state enumeration. - Hyunwoo Cho; Gary D. Hachtel; Fabio Somenzi (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1993)

Probabilistic Analysis of Large Finite State Machines. - Gary D. Hachtel; Enrico Macii; Abelardo Pardo; Fabio Somenzi (DAC, 1994)

Timing Analysis of Combinational Circuits using ADD's. - R. Iris Bahar; Hyunwoo Cho; Gary D. Hachtel; Enrico Macii; Fabio Somenzi (EDAC-ETC-EUROASIC, 1994)

A State Space Decomposition Algorithm for Approximate FSM Traversal. - Hyunwoo Cho; Gary D. Hachtel; Enrico Macii; Massimo Poncino; Fabio Somenzi (EDAC-ETC-EUROASIC, 1994)

Symbolic Algorithms to Calculate Steady-State Probabilities of a Finite State Machine. - Gary D. Hachtel; Enrico Macii; Abelardo Pardo; Fabio Somenzi (EDAC-ETC-EUROASIC, 1994)

An ADD-based algorithm for shortest path back-tracing of large graphs. - R. Iris Bahar; Gary D. Hachtel; Abelardo Pardo; Massimo Poncino; Fabio Somenzi (Great Lakes Symposium on VLSI, 1994)

A symbolic method to reduce power consumption of circuits containing false paths. - R. Iris Bahar; Gary D. Hachtel; Enrico Macii; Fabio Somenzi (ICCAD, 1994)

Re-encoding sequential circuits to reduce power dissipation. - Gary D. Hachtel; Mariano Hermida de la Rica; Abelardo Pardo; Massimo Poncino; Fabio Somenzi (ICCAD, 1994)

Symmetry detection and dynamic variable ordering of decision diagrams. - Shipra Panda; Fabio Somenzi; Bernard Plessier (ICCAD, 1994)

A Structural Approach to State Space Decomposition for Approximate Reachability Analysis. - Hyunwoo Cho; Gary D. Hachtel; Enrico Macii; Massimo Poncino; Fabio Somenzi (ICCD, 1994)

Extended BDDs: Trading off Canonicity for Structure in Verification Algorithms. - Bernard Plessier; Gary D. Hachtel; Fabio Somenzi (Formal Methods Syst. Des., 1994)

Exact and heuristic algorithms for the minimization of incompletely specified state machines. - June-Kyung Rho; Gary D. Hachtel; Fabio Somenzi; Reily M. Jacoby (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1994)

Don't care sequences and the optimization of interacting finite state machines. - June-Kyung Rho; Fabio Somenzi (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1994)

Computing the Maximum Power Cycles of a Sequential Circuit. - Srilatha Manne; Abelardo Pardo; R. Iris Bahar; Gary D. Hachtel; Fabio Somenzi; Enrico Macii; Massimo Poncino (DAC, 1995)

Boolean techniques for low power driven re-synthesis. - R. Iris Bahar; Fabio Somenzi (ICCAD, 1995)

Who are the variables in your neighborhood. - Shipra Panda; Fabio Somenzi (ICCAD, 1995)

High-density reachability analysis. - Kavita Ravi; Fabio Somenzi (ICCAD, 1995)

CMOS dynamic power estimation based on collapsible current source transistor modeling. - Abelardo Pardo; R. Iris Bahar; Srilatha Manne; Peter Feldmann; Gary D. Hachtel; Fabio Somenzi (ISLPD, 1995)

Logic synthesis and verification algorithms. - Gary D. Hachtel; Fabio Somenzi (Kluwer, 1996)

VIS: A System for Verification and Synthesis. - 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 001; et al. (CAV, 1996)

VIS. - 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 001; et al. (FMCAD, 1996)

Modular Verification of Multipliers. - Kavita Ravi; Abelardo Pardo; Gary D. Hachtel; Fabio Somenzi (FMCAD, 1996)

Tearing based automatic abstraction for CTL model checking. - Woohyuk Lee; Abelardo Pardo; Jae-Young Jang; Gary D. Hachtel; Fabio Somenzi (ICCAD, 1996)

Symbolic computation of logic implications for technology-dependent low-power synthesis. - R. Iris Bahar; M. Burns; Gary D. Hachtel; Enrico Macii; H. Shin; Fabio Somenzi (ISLPED, 1996)

Automatic state space decomposition for approximate FSM traversal based on circuit analysis. - Hyunwoo Cho; Gary D. Hachtel; Enrico Macii; Massimo Poncino; Fabio Somenzi (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1996)

Algorithms for approximate FSM traversal based on state space decomposition. - Hyunwoo Cho; Gary D. Hachtel; Enrico Macii; Bernard Plessier; Fabio Somenzi (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1996)

Markovian analysis of large finite state machines. - Gary D. Hachtel; Enrico Macii; Abelardo Pardo; Fabio Somenzi (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1996)

Linear Sifting of Decision Diagrams - Christoph Meinel; Fabio Somenzi; Thorsten Theobald (Universität Trier, Mathematik/Informatik, Forschungsbericht, 1996)

Remembrance of Things Past: Locality and Memory in BDDs. - Srilatha Manne; Dirk Grunwald; Fabio Somenzi (DAC, 1997)

A symbolic algorithm for low-power sequential synthesis. - Balakrishna Kumthekar; In-Ho Moon; Fabio Somenzi (ISLPED, 1997)

Algebraic Decision Diagrams and Their Applications. - R. Iris Bahar; Erica A. Frohm; Charles M. Gaona; Gary D. Hachtel; Enrico Macii; Abelardo Pardo; Fabio Somenzi (Formal Methods Syst. Des., 1997)

A Symbolic Algorithms for Maximum Flow in 0-1 Networks. - Gary D. Hachtel; Fabio Somenzi (Formal Methods Syst. Des., 1997)

Arithmetic Boolean Expression Manipulator Using BDDs. - Shin-ichi Minato; Fabio Somenzi (Formal Methods Syst. Des., 1997)

Symbolic timing analysis and resynthesis for low power of combinational circuits containing false paths. - R. Iris Bahar; Hyunwoo Cho; Gary D. Hachtel; Enrico Macii; Fabio Somenzi (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1997)

Formal verification of digital systems by automatic reduction of data paths. - Enrico Macii; Bernard Plessier; Fabio Somenzi (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1997)

Function Decomposition and Synthesis Using Linear Sifting - Christoph Meinel; Fabio Somenzi; Thorsten Theobald (Universität Trier, Mathematik/Informatik, Forschungsbericht, 1997)

In-Place Power Optimization for LUT-Based FPGAs. - Balakrishna Kumthekar; Luca Benini; Enrico Macii; Fabio Somenzi (DAC, 1998)

Approximation and Decomposition of Binary Decision Diagrams. - Kavita Ravi; Kenneth L. McMillan; Thomas R. Shiple; Fabio Somenzi (DAC, 1998)

A Performance Study of BDD-Based Model Checking. - Bwolen Yang; Randal E. Bryant; David R. O'Hallaron; Armin Biere; Olivier Coudert; Geert Janssen; Rajeev K. Ranjan 001; Fabio Somenzi (FMCAD, 1998)

Symbolic algorithms for layout-oriented synthesis of pass transistor logic circuits. - Fabrizio Ferrandi; Alberto Macii; Enrico Macii; Massimo Poncino; Riccardo Scarsi; Fabio Somenzi (ICCAD, 1998)

Approximate reachability don't cares for CTL model checking. - In-Ho Moon; Jae-Young Jang; Gary D. Hachtel; Fabio Somenzi; Jun Yuan 007; Carl Pixley (ICCAD, 1998)

On the optimization power of retiming and resynthesis transformations. - Rajeev K. Ranjan 001; Vigyan Singhal; Fabio Somenzi; Robert K. Brayton (ICCAD, 1998)

High-level power modeling, estimation, and optimization. - Enrico Macii; Massoud Pedram; Fabio Somenzi (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1998)

Efficient Decision Procedures for Model Checking of Linear Time Logic Properties. - Roderick Bloem; Kavita Ravi; Fabio Somenzi (CAV, 1999)

Hints to accelerate Symbolic Traversal. - Kavita Ravi; Fabio Somenzi (CHARME, 1999)

Using Combinational Verification for Sequential Circuits. - Rajeev K. Ranjan 001; Vigyan Singhal; Fabio Somenzi; Robert K. Brayton (DATE, 1999)

Lazy group sifting for efficient symbolic state traversal of FSMs. - Hiroyuki Higuchi; Fabio Somenzi (ICCAD, 1999)

Least fixpoint approximations for reachability analysis. - In-Ho Moon; James H. Kukula; Thomas R. Shiple; Fabio Somenzi (ICCAD, 1999)

Efficient Fixpoint Computation for Invariant Checking. - Kavita Ravi; Fabio Somenzi (ICCD, 1999)

Symbolic State Exploration. - Fabio Somenzi (SMC@FLoC, 1999)

Efficient Büchi Automata from LTL Formulae. - Fabio Somenzi; Roderick Bloem (CAV, 2000)

Symbolic guided search for CTL model checking. - Roderick Bloem; Kavita Ravi; Fabio Somenzi (DAC, 2000)

Optimizing sequential verification by retiming transformations. - Gianpiero Cabodi; Stefano Quer; Fabio Somenzi (DAC, 2000)

To split or to conjoin: the question in image computation. - In-Ho Moon; James H. Kukula; Kavita Ravi; Fabio Somenzi (DAC, 2000)

Power and Delay Reduction via Simultaneous Logic and Placement Optimization in FPGAs. - Balakrishna Kumthekar; Fabio Somenzi (DATE, 2000)

Border-Block Triangular Form and Conjunction Schedule in Image Computation. - In-Ho Moon; Gary D. Hachtel; Fabio Somenzi (FMCAD, 2000)

A Comparative Study of Symbolic Algorithms for the Computation of Fair Cycles. - Kavita Ravi; Roderick Bloem; Fabio Somenzi (FMCAD, 2000)

Fundamental CAD algorithms. - Melvin A. Breuer; Majid Sarrafzadeh; Fabio Somenzi (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2000)

Linear sifting of decision diagrams and its application insynthesis. - Christoph Meinel; Fabio Somenzi; Thorsten Theobald (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2000)

Divide and Compose: SCC Refinement for Language Emptiness. - Chao Wang 001; Roderick Bloem; Gary D. Hachtel; Kavita Ravi; Fabio Somenzi (CONCUR, 2001)

Efficient manipulation of decision diagrams. - Fabio Somenzi (Int. J. Softw. Tools Technol. Transf., 2001)

Using lower bounds during dynamic BDD minimization. - Rolf Drechsler; Wolfgang Günther 001; Fabio Somenzi (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2001)

Fair Simulation Minimization. - Sankar Gurumurthy; Roderick Bloem; Fabio Somenzi (CAV, 2002)

Vacuum Cleaning CTL Formulae. - Mitra Purandare; Fabio Somenzi (CAV, 2002)

Analysis of Symbolic SCC Hull Algorithms. - Fabio Somenzi; Kavita Ravi; Roderick Bloem (FMCAD, 2002)

Fine-Grain Conjunction Scheduling for Symbolic Reachability Analysis. - HoonSang Jin; Andreas Kuehlmann; Fabio Somenzi (TACAS, 2002)

On Complementing Nondeterministic Büchi Automata. - Sankar Gurumurthy; Orna Kupferman; Fabio Somenzi; Moshe Y. Vardi (CHARME, 2003)

The Charme of Abstract Entities. - Fabio Somenzi (CHARME, 2003)

Formal verification - prove it or pitch it. - Rajesh K. Gupta 001; Shishpal Rawat; Sandeep K. Shukla; Brian Bailey; Daniel K. Beece; Masahiro Fujita; Carl Pixley; John O'Leary; Fabio Somenzi (DAC, 2003)

Dos and don'ts of CTL state coverage estimation. - Nikhil Jayakumar; Mitra Purandare; Fabio Somenzi (DAC, 2003)

The Compositional Far Side of Image Computation. - Chao Wang 001; Gary D. Hachtel; Fabio Somenzi (ICCAD, 2003)

Improving Ariadneýs Bundle by Following Multiple Threads in Abstraction Refinement. - Chao Wang 001; Bing Li; HoonSang Jin; Gary D. Hachtel; Fabio Somenzi (ICCAD, 2003)

A satisfiability-based approach to abstraction refinement in model checking. - Bing Li; Chao Wang 001; Fabio Somenzi (BMC@CAV, 2003)

Proving More Properties with Bounded Model Checking. - Mohammad Awedh; Fabio Somenzi (CAV, 2004)

CirCUs: A Satisfiability Solver Geared towards Bounded Model Checking. - HoonSang Jin; Mohammad Awedh; Fabio Somenzi (CAV, 2004)

Refining the SAT decision ordering for bounded model checking. - Chao Wang 001; HoonSang Jin; Gary D. Hachtel; Fabio Somenzi (DAC, 2004)

Increasing the Robustness of Bounded Model Checking by Computing Lower Bounds on the Reachable States. - Mohammad Awedh; Fabio Somenzi (FMCAD, 2004)

Efficient computation of small abstraction refinements. - Bing Li; Fabio Somenzi (ICCAD, 2004)

Fine-Grain Abstraction and Sequential Don't Cares for Large Scale Model Checking. - Chao Wang 001; Gary D. Hachtel; Fabio Somenzi (ICCD, 2004)

CirCUs: A Hybrid Satisfiability Solver. - HoonSang Jin; Fabio Somenzi (SAT, 2004)

Minimal Assignments for Bounded Model Checking. - Kavita Ravi; Fabio Somenzi (TACAS, 2004)

An Incremental Algorithm to Check Satisfiability for Bounded Model Checking. - HoonSang Jin; Fabio Somenzi (BMC@CAV, 2004)

Fate and free will in error traces. - HoonSang Jin; Kavita Ravi; Fabio Somenzi (Int. J. Softw. Tools Technol. Transf., 2004)

Automatic Generation of Hints for Symbolic Traversal. - David Ward; Fabio Somenzi (CHARME, 2005)

Prime clauses for fast enumeration of satisfying assignments to boolean circuits. - HoonSang Jin; Fabio Somenzi (DAC, 2005)

Efficient Conflict Analysis for Finding All Satisfying Assignments of a Boolean Circuit. - HoonSang Jin; HyoJung Han; Fabio Somenzi (TACAS, 2005)

Termination Criteria for Bounded Model Checking: Extensions and Comparison. - Mohammad Awedh; Fabio Somenzi (BMC@CAV, 2005)

Abstraction refinement in symbolic model checking using satisfiability as the only decision procedure. - Bing Li; Chao Wang 001; Fabio Somenzi (Int. J. Softw. Tools Technol. Transf., 2005)

Logic synthesis and verification algorithms. - Gary D. Hachtel; Fabio Somenzi (Springer, 2006)

Automatic invariant strengthening to prove properties in bounded model checking. - Mohammad Awedh; Fabio Somenzi (DAC, 2006)

Guiding simulation with increasingly refined abstract traces. - Kuntal Nanshi; Fabio Somenzi (DAC, 2006)

Strong conflict analysis for propositional satisfiability. - HoonSang Jin; Fabio Somenzi (DATE, 2006)

Finite Instantiations for Integer Difference Logic. - Hyondeuk Kim; Fabio Somenzi (FMCAD, 2006)

Decomposing image computation for symbolic reachability analysis using control flow information. - David Ward; Fabio Somenzi (ICCAD, 2006)

Efficient Abstraction Refinement in Interpolation-Based Unbounded Model Checking. - Bing Li; Fabio Somenzi (TACAS, 2006)

Preface. - Roderick Bloem; Marco Roveri; Fabio Somenzi (V&D@FLoC, 2006)

An Algorithm for Strongly Connected Component Analysis in n log n Symbolic Steps. - Roderick Bloem; Harold N. Gabow; Fabio Somenzi (Formal Methods Syst. Des., 2006)

Compositional SCC Analysis for Language Emptiness. - Chao Wang 001; Roderick Bloem; Gary D. Hachtel; Kavita Ravi; Fabio Somenzi (Formal Methods Syst. Des., 2006)

Improving Ariadne's Bundle by Following Multiple Threads in Abstraction Refinement. - Chao Wang 001; Bing Li; HoonSang Jin; Gary D. Hachtel; Fabio Somenzi (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2006)

Abstraction Refinement for Large Scale Model Checking - Chao Wang 001; Gary D. Hachtel; Fabio Somenzi (Springer, 2006)

Alembic: An Efficient Algorithm for CNF Preprocessing. - HyoJung Han; Fabio Somenzi (DAC, 2007)

Disequality Management in Integer Difference Logic via Finite Instantiations. - Hyondeuk Kim; HoonSang Jin; Fabio Somenzi (J. Satisf. Boolean Model. Comput., 2007)

Application of Formal Word-Level Analysis to Constrained Random Simulation. - Hyondeuk Kim; HoonSang Jin; Kavita Ravi; Petr Spacek; John Pierce; Robert P. Kurshan; Fabio Somenzi (CAV, 2008)

Improved Visibility in One-to-Many Trace Concretization. - Kuntal Nanshi; Fabio Somenzi (DATE, 2008)

A Hybrid Algorithm for LTL Games. - Saqib Sohail; Fabio Somenzi; Kavita Ravi (VMCAI, 2008)

Constraints in one-to-many concretization for abstraction refinement. - Kuntal Nanshi; Fabio Somenzi (DAC, 2009)

Safety first: A two-stage algorithm for LTL games. - Saqib Sohail; Fabio Somenzi (FMCAD, 2009)

On-the-Fly Clause Improvement. - HyoJung Han; Fabio Somenzi (SAT, 2009)

Efficient Term-ITE Conversion for Satisfiability Modulo Theories. - Hyondeuk Kim; Fabio Somenzi; HoonSang Jin (SAT, 2009)

Making Deduction More Effective in SAT Solvers. - HyoJung Han; Fabio Somenzi; HoonSang Jin (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2010)

Clause simplification through dominator analysis. - HyoJung Han; HoonSang Jin; Fabio Somenzi (DATE, 2011)

An incremental approach to model checking progress properties. - Aaron R. Bradley; Fabio Somenzi; Zyad Hassan; Yan Zhang 027 (FMCAD, 2011)

A Study of Sweeping Algorithms in the Context of Model Checking. - Zyad Hassan; Yan Zhang 027; Fabio Somenzi (DIFTS@FMCAD, 2011)

IC3: where monolithic and incremental meet. - Fabio Somenzi; Aaron R. Bradley (FMCAD, 2011)

Incremental, Inductive CTL Model Checking. - Zyad Hassan; Aaron R. Bradley; Fabio Somenzi (CAV, 2012)

Piecewise linear modeling of nonlinear devices for formal verification of analog circuits. - Yan Zhang 027; Sriram Sankaranarayanan 001; Fabio Somenzi (FMCAD, 2012)

Better generalization in IC3. - Zyad Hassan; Aaron R. Bradley; Fabio Somenzi (FMCAD, 2013)

Efficient handling of obligation constraints in synthesis from omega-regular specifications. - Saqib Sohail; Fabio Somenzi (FMCAD, 2013)

From statistical model checking to statistical model inference: characterizing the effect of process variations in analog circuits. - Yan Zhang 027; Sriram Sankaranarayanan 001; Fabio Somenzi; Xin Chen 002; Erika Ábrahám (ICCAD, 2013)

Safety first: a two-stage algorithm for the synthesis of reactive systems. - Saqib Sohail; Fabio Somenzi (Int. J. Softw. Tools Technol. Transf., 2013)

Using Abstraction to Guide the Search for Long Error Traces. - Kuntal Nanshi; Fabio Somenzi (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2013)

Sparse statistical model inference for analog circuits under process variations. - Yan Zhang 027; Sriram Sankaranarayanan 001; Fabio Somenzi (ASP-DAC, 2014)

Statistically Sound Verification and Optimization for Complex Systems. - Yan Zhang 027; Sriram Sankaranarayanan 001; Fabio Somenzi (ATVA, 2014)

Proving Parameterized Systems Safe by Generalizing Clausal Proofs of Small Instances. - Michael Dooley; Fabio Somenzi (CAV (1), 2016)

The Reach-Avoid Problem for Constant-Rate Multi-mode Systems. - Shankara Narayanan Krishna; Aviral Kumar; Fabio Somenzi; Behrouz Touri; Ashutosh Trivedi 001 (ATVA, 2017)

Global Almost-Sure Reachability in Stochastic Constant-Rate Multi-Mode Systems. - Fabio Somenzi; Behrouz Touri; Ashutosh Trivedi 001 (HSCC, 2018)

Reinforcement Learning and Formal Requirements. - Fabio Somenzi; Ashutosh Trivedi 001 (NSV@CAV, 2019)

Limit reachability for model-free reinforcement learning of ω-regular objectives. - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (SNR, 2019)

Omega-Regular Objectives in Model-Free Reinforcement Learning. - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (TACAS (1), 2019)

Good-for-MDPs Automata. - Ernst Moritz Hahn; Mateo Perez; Fabio Somenzi; Ashutosh Trivedi 001; Sven Schewe; Dominik Wojtczak (CoRR, 2019)

Faithful and Effective Reward Schemes for Model-Free Reinforcement Learning of Omega-Regular Objectives. - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (ATVA, 2020)

Model-Free Reinforcement Learning for Stochastic Parity Games. - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (CONCUR, 2020)

Formal Controller Synthesis for Continuous-Space MDPs via Model-Free Reinforcement Learning. - Abolfazl Lavaei; Fabio Somenzi; Sadegh Soudjani; Ashutosh Trivedi 001; Majid Zamani 001 (ICCPS, 2020)

Good-for-MDPs Automata for Probabilistic Analysis and Reinforcement Learning. - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (TACAS (1), 2020)

Reward Shaping for Reinforcement Learning with Omega-Regular Objectives. - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (CoRR, 2020)

Model-Free Reinforcement Learning for Branching Markov Decision Processes. - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (CAV (2), 2021)

Model-Free Reinforcement Learning for Lexicographic Omega-Regular Objectives. - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (FM, 2021)

Mungojerrie: Reinforcement Learning of Linear-Time Objectives. - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (CoRR, 2021)

Model-free Reinforcement Learning for Branching Markov Decision Processes (Artifact Evaluation for CAV 2021). - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (Zenodo, 2021)

Translating Omega-Regular Specifications to Average Objectives for Model-Free Reinforcement Learning. - Milad Kazemi; Mateo Perez; Fabio Somenzi; Sadegh Soudjani; Ashutosh Trivedi 001; Alvaro Velasquez (AAMAS, 2022)

An Impossibility Result in Automata-Theoretic Reinforcement Learning. - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (ATVA, 2022)

Alternating Good-for-MDPs Automata. - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (ATVA, 2022)

Reinforcement Learning with Guarantees that Hold for Ever. - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (FMICS, 2022)

Recursive Reinforcement Learning. - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (NeurIPS, 2022)

Alternating Good-for-MDP Automata. - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (CoRR, 2022)

Compositional Reinforcement Learning for Discrete-Time Stochastic Control Systems. - Abolfazl Lavaei; Mateo Perez; Milad Kazemi; Fabio Somenzi; Sadegh Soudjani; Ashutosh Trivedi 001; Majid Zamani 001 (CoRR, 2022)

Policy Synthesis and Reinforcement Learning for Discounted LTL. - Rajeev Alur; Osbert Bastani; Kishor Jothimurugan; Mateo Perez; Fabio Somenzi; Ashutosh Trivedi 001 (CAV (1), 2023)

Omega-Regular Reward Machines. - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (ECAI, 2023)

Mungojerrie: Linear-Time Objectives in Model-Free Reinforcement Learning. - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (TACAS (1), 2023)

Multi-objective ω-Regular Reinforcement Learning. - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (Formal Aspects Comput., 2023)

Artifact for "Assume-Guarantee Reinforcement Learning". - Milad Kazemi Mehrabadi; Mateo Perez; Fabio Somenzi; Sadegh Soudjani; Ashutosh Trivedi 001; Alvaro Velasquez (Zenodo, 2023)

Omega-Regular Decision Processes. - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (AAAI, 2024)

Assume-Guarantee Reinforcement Learning. - Milad Kazemi; Mateo Perez; Fabio Somenzi; Sadegh Soudjani; Ashutosh Trivedi 001; Alvaro Velasquez (AAAI, 2024)

A PAC Learning Algorithm for LTL and Omega-Regular Objectives in MDPs. - Mateo Perez; Fabio Somenzi; Ashutosh Trivedi 001 (AAAI, 2024)

Regular Reinforcement Learning. - Taylor Dohmen; Mateo Perez; Fabio Somenzi; Ashutosh Trivedi 001 (CAV (3), 2024)

Multi-Agent Reinforcement Learning for Alternating-Time Logic. - Ernst Moritz Hahn; Mateo Perez; Sven Schewe; Fabio Somenzi; Ashutosh Trivedi 001; Dominik Wojtczak (ECAI, 2024)

Explaining Puzzle Solutions in Natural Language: An Exploratory Study on 6x6 Sudoku. - Anirudh Maiya; Razan Alghamdi; Maria Leonor Pacheco; Ashutosh Trivedi 001; Fabio Somenzi (ACL (Findings), 2025)

Average Reward Reinforcement Learning for Omega-Regular and Mean-Payoff Objectives. - Milad Kazemi; Mateo Perez; Fabio Somenzi; Sadegh Soudjani; Ashutosh Trivedi 001; Alvaro Velasquez (CoRR, 2025)

Explaining Hitori Puzzles: Neurosymbolic Proof Staging for Sequential Decisions. - Maria Leonor Pacheco; Fabio Somenzi; Dananjay Srinivas; Ashutosh Trivedi 001 (CoRR, 2025)