| 2025 | ACL | Explaining Puzzle Solutions in Natural Language: An Exploratory Study on 6x6 Sudoku. | Anirudh Maiya, Razan Alghamdi, Maria Leonor Pacheco, Ashutosh Trivedi, Fabio Somenzi |
| 2024 | AAAI | Omega-Regular Decision Processes. | Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak |
| 2024 | AAAI | Assume-Guarantee Reinforcement Learning. | Milad Kazemi, Mateo Perez, Fabio Somenzi, Sadegh Soudjani, Ashutosh Trivedi, Alvaro Velasquez |
| 2024 | AAAI | A PAC Learning Algorithm for LTL and Omega-Regular Objectives in MDPs. | Mateo Perez, Fabio Somenzi, Ashutosh Trivedi |
| 2024 | CAV | Regular Reinforcement Learning. | Taylor Dohmen, Mateo Perez, Fabio Somenzi, Ashutosh Trivedi |
| 2024 | ECAI | Multi-Agent Reinforcement Learning for Alternating-Time Logic. | Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak |
| 2023 | CAV | Policy Synthesis and Reinforcement Learning for Discounted LTL. | Rajeev Alur, Osbert Bastani, Kishor Jothimurugan, Mateo Perez, Fabio Somenzi, Ashutosh Trivedi |
| 2023 | ECAI | Omega-Regular Reward Machines. | Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak |
| 2023 | TACAS | Mungojerrie: Linear-Time Objectives in Model-Free Reinforcement Learning. | Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak |
| 2022 | ATVA | An Impossibility Result in Automata-Theoretic Reinforcement Learning. | Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak |
| 2022 | ATVA | Alternating Good-for-MDPs Automata. | Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak |
| 2022 | FMICS | Reinforcement Learning with Guarantees that Hold for Ever. | Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak |
| 2021 | CAV | Model-Free Reinforcement Learning for Branching Markov Decision Processes. | Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak |
| 2021 | FM | Model-Free Reinforcement Learning for Lexicographic Omega-Regular Objectives. | Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak |
| 2020 | ATVA | 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, Dominik Wojtczak |
| 2020 | CONCUR | Model-Free Reinforcement Learning for Stochastic Parity Games. | Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak |
| 2020 | TACAS | Good-for-MDPs Automata for Probabilistic Analysis and Reinforcement Learning. | Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak |
| 2019 | CAV | Reinforcement Learning and Formal Requirements. | Fabio Somenzi, Ashutosh Trivedi |
| 2019 | TACAS | Omega-Regular Objectives in Model-Free Reinforcement Learning. | Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak |
| 2017 | ATVA | The Reach-Avoid Problem for Constant-Rate Multi-mode Systems. | Shankara Narayanan Krishna, Aviral Kumar, Fabio Somenzi, Behrouz Touri, Ashutosh Trivedi |
| 2016 | CAV | Proving Parameterized Systems Safe by Generalizing Clausal Proofs of Small Instances. | Michael Dooley, Fabio Somenzi |
| 2014 | ASPDAC | Sparse statistical model inference for analog circuits under process variations. | Yan Zhang, Sriram Sankaranarayanan, Fabio Somenzi |
| 2014 | ATVA | Statistically Sound Verification and Optimization for Complex Systems. | Yan Zhang, Sriram Sankaranarayanan, Fabio Somenzi |
| 2013 | FMCAD | Better generalization in IC3. | Zyad Hassan, Aaron R. Bradley, Fabio Somenzi |
| 2013 | FMCAD | Efficient handling of obligation constraints in synthesis from omega-regular specifications. | Saqib Sohail, Fabio Somenzi |
| 2013 | ICCAD | From statistical model checking to statistical model inference: characterizing the effect of process variations in analog circuits. | Yan Zhang, Sriram Sankaranarayanan, Fabio Somenzi, Xin Chen, Erika brahm |
| 2012 | CAV | Incremental, Inductive CTL Model Checking. | Zyad Hassan, Aaron R. Bradley, Fabio Somenzi |
| 2012 | FMCAD | Piecewise linear modeling of nonlinear devices for formal verification of analog circuits. | Yan Zhang, Sriram Sankaranarayanan, Fabio Somenzi |
| 2011 | DATE | Clause simplification through dominator analysis. | HyoJung Han, HoonSang Jin, Fabio Somenzi |
| 2011 | FMCAD | An incremental approach to model checking progress properties. | Aaron R. Bradley, Fabio Somenzi, Zyad Hassan, Yan Zhang |
| 2011 | FMCAD | A Study of Sweeping Algorithms in the Context of Model Checking. | Zyad Hassan, Yan Zhang, Fabio Somenzi |
| 2011 | FMCAD | IC3: where monolithic and incremental meet. | Fabio Somenzi, Aaron R. Bradley |
| 2009 | DAC | Constraints in one-to-many concretization for abstraction refinement. | Kuntal Nanshi, Fabio Somenzi |
| 2009 | FMCAD | Safety first: A two-stage algorithm for LTL games. | Saqib Sohail, Fabio Somenzi |
| 2009 | SAT | On-the-Fly Clause Improvement. | HyoJung Han, Fabio Somenzi |
| 2009 | SAT | Efficient Term-ITE Conversion for Satisfiability Modulo Theories. | Hyondeuk Kim, Fabio Somenzi, HoonSang Jin |
| 2008 | CAV | 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 |
| 2008 | DATE | Improved Visibility in One-to-Many Trace Concretization. | Kuntal Nanshi, Fabio Somenzi |
| 2008 | VMCAI | A Hybrid Algorithm for LTL Games. | Saqib Sohail, Fabio Somenzi, Kavita Ravi |
| 2007 | DAC | Alembic: An Efficient Algorithm for CNF Preprocessing. | HyoJung Han, Fabio Somenzi |
| 2006 | DAC | Automatic invariant strengthening to prove properties in bounded model checking. | Mohammad Awedh, Fabio Somenzi |
| 2006 | DAC | Guiding simulation with increasingly refined abstract traces. | Kuntal Nanshi, Fabio Somenzi |
| 2006 | DATE | Strong conflict analysis for propositional satisfiability. | HoonSang Jin, Fabio Somenzi |
| 2006 | FMCAD | Finite Instantiations for Integer Difference Logic. | Hyondeuk Kim, Fabio Somenzi |
| 2006 | ICCAD | Decomposing image computation for symbolic reachability analysis using control flow information. | David Ward, Fabio Somenzi |
| 2006 | TACAS | Efficient Abstraction Refinement in Interpolation-Based Unbounded Model Checking. | Bing Li, Fabio Somenzi |
| 2005 | DAC | Prime clauses for fast enumeration of satisfying assignments to boolean circuits. | HoonSang Jin, Fabio Somenzi |
| 2005 | TACAS | Efficient Conflict Analysis for Finding All Satisfying Assignments of a Boolean Circuit. | HoonSang Jin, HyoJung Han, Fabio Somenzi |
| 2004 | CAV | Proving More Properties with Bounded Model Checking. | Mohammad Awedh, Fabio Somenzi |
| 2004 | CAV | CirCUs: A Satisfiability Solver Geared towards Bounded Model Checking. | HoonSang Jin, Mohammad Awedh, Fabio Somenzi |
| 2004 | DAC | Refining the SAT decision ordering for bounded model checking. | Chao Wang, HoonSang Jin, Gary D. Hachtel, Fabio Somenzi |
| 2004 | FMCAD | Increasing the Robustness of Bounded Model Checking by Computing Lower Bounds on the Reachable States. | Mohammad Awedh, Fabio Somenzi |
| 2004 | ICCAD | Efficient computation of small abstraction refinements. | Bing Li, Fabio Somenzi |
| 2004 | ICCD | Fine-Grain Abstraction and Sequential Don't Cares for Large Scale Model Checking. | Chao Wang, Gary D. Hachtel, Fabio Somenzi |
| 2004 | SAT | CirCUs: A Hybrid Satisfiability Solver. | HoonSang Jin, Fabio Somenzi |
| 2004 | SAT | CirCUs: A Hybrid Satisfiability Solver. | HoonSang Jin, Fabio Somenzi |
| 2004 | TACAS | Minimal Assignments for Bounded Model Checking. | Kavita Ravi, Fabio Somenzi |
| 2003 | DAC | Formal verification - prove it or pitch it. | Rajesh K. Gupta, Shishpal Rawat, Sandeep K. Shukla, Brian Bailey, Daniel K. Beece, Masahiro Fujita, Carl Pixley, John O'Leary, Fabio Somenzi |
| 2003 | DAC | Dos and don'ts of CTL state coverage estimation. | Nikhil Jayakumar, Mitra Purandare, Fabio Somenzi |
| 2003 | ICCAD | The Compositional Far Side of Image Computation. | Chao Wang, Gary D. Hachtel, Fabio Somenzi |
| 2003 | ICCAD | Improving Ariadnes Bundle by Following Multiple Threads in Abstraction Refinement. | Chao Wang, Bing Li, HoonSang Jin, Gary D. Hachtel, Fabio Somenzi |
| 2002 | CAV | Fair Simulation Minimization. | Sankar Gurumurthy, Roderick Bloem, Fabio Somenzi |
| 2002 | CAV | Vacuum Cleaning CTL Formulae. | Mitra Purandare, Fabio Somenzi |
| 2002 | FMCAD | Analysis of Symbolic SCC Hull Algorithms. | Fabio Somenzi, Kavita Ravi, Roderick Bloem |
| 2002 | TACAS | Fine-Grain Conjunction Scheduling for Symbolic Reachability Analysis. | HoonSang Jin, Andreas Kuehlmann, Fabio Somenzi |
| 2002 | TACAS | Fate and Free Will in Error Traces. | HoonSang Jin, Kavita Ravi, Fabio Somenzi |
| 2001 | CONCUR | Divide and Compose: SCC Refinement for Language Emptiness. | Chao Wang, Roderick Bloem, Gary D. Hachtel, Kavita Ravi, Fabio Somenzi |
| 2000 | CAV | Efficient Bchi Automata from LTL Formulae. | Fabio Somenzi, Roderick Bloem |
| 2000 | DAC | Symbolic guided search for CTL model checking. | Roderick Bloem, Kavita Ravi, Fabio Somenzi |
| 2000 | DAC | Optimizing sequential verification by retiming transformations. | Gianpiero Cabodi, Stefano Quer, Fabio Somenzi |
| 2000 | DAC | To split or to conjoin: the question in image computation. | In-Ho Moon, James H. Kukula, Kavita Ravi, Fabio Somenzi |
| 2000 | DATE | Power and Delay Reduction via Simultaneous Logic and Placement Optimization in FPGAs. | Balakrishna Kumthekar, Fabio Somenzi |
| 2000 | FMCAD | An Algorithm for Strongly Connected Component Analysis in | Roderick Bloem, Harold N. Gabow, Fabio Somenzi |
| 2000 | FMCAD | Border-Block Triangular Form and Conjunction Schedule in Image Computation. | In-Ho Moon, Gary D. Hachtel, Fabio Somenzi |
| 2000 | FMCAD | A Comparative Study of Symbolic Algorithms for the Computation of Fair Cycles. | Kavita Ravi, Roderick Bloem, Fabio Somenzi |
| 1999 | CAV | Efficient Decision Procedures for Model Checking of Linear Time Logic Properties. | Roderick Bloem, Kavita Ravi, Fabio Somenzi |
| 1999 | DATE | Using Combinational Verification for Sequential Circuits. | Rajeev K. Ranjan, Vigyan Singhal, Fabio Somenzi, Robert K. Brayton |
| 1999 | ICCAD | Lazy group sifting for efficient symbolic state traversal of FSMs. | Hiroyuki Higuchi, Fabio Somenzi |
| 1999 | ICCAD | Least fixpoint approximations for reachability analysis. | In-Ho Moon, James H. Kukula, Thomas R. Shiple, Fabio Somenzi |
| 1999 | ICCD | Efficient Fixpoint Computation for Invariant Checking. | Kavita Ravi, Fabio Somenzi |
| 1998 | ASPDAC | Function Decomposition and Synthesis Using Linear Sifting. | Christoph Meinel, Fabio Somenzi, Thorsten Theobald |
| 1998 | DAC | In-Place Power Optimization for LUT-Based FPGAs. | Balakrishna Kumthekar, Luca Benini, Enrico Macii, Fabio Somenzi |
| 1998 | DAC | Approximation and Decomposition of Binary Decision Diagrams. | Kavita Ravi, Kenneth L. McMillan, Thomas R. Shiple, Fabio Somenzi |
| 1998 | FMCAD | 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, Fabio Somenzi |
| 1998 | ICCAD | Symbolic algorithms for layout-oriented synthesis of pass transistor logic circuits. | Fabrizio Ferrandi, Alberto Macii, Enrico Macii, Massimo Poncino, Riccardo Scarsi, Fabio Somenzi |
| 1998 | ICCAD | Approximate reachability don't cares for CTL model checking. | In-Ho Moon, Jae-Young Jang, Gary D. Hachtel, Fabio Somenzi, Jun Yuan, Carl Pixley |
| 1998 | ICCAD | On the optimization power of retiming and resynthesis transformations. | Rajeev K. Ranjan, Vigyan Singhal, Fabio Somenzi, Robert K. Brayton |
| 1997 | DAC | High-Level Power Modeling, Estimation, and Optimization. | Enrico Macii, Massoud Pedram, Fabio Somenzi |
| 1997 | DAC | Remembrance of Things Past: Locality and Memory in BDDs. | Srilatha Manne, Dirk Grunwald, Fabio Somenzi |
| 1997 | DAC | Linear Sifting of Decision Diagrams. | Christoph Meinel, Fabio Somenzi, Thorsten Theobald |
| 1997 | ISLPED | A symbolic algorithm for low-power sequential synthesis. | Balakrishna Kumthekar, In-Ho Moon, Fabio Somenzi |
| 1996 | CAV | 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, Shaker Sarwary, Thomas R. Shiple, Gitanjali Swamy, Tiziano Villa |
| 1996 | FMCAD | 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, Shaker Sarwary, Thomas R. Shiple, Gitanjali Swamy, Tiziano Villa |
| 1996 | FMCAD | Modular Verification of Multipliers. | Kavita Ravi, Abelardo Pardo, Gary D. Hachtel, Fabio Somenzi |
| 1996 | ICCAD | Tearing based automatic abstraction for CTL model checking. | Woohyuk Lee, Abelardo Pardo, Jae-Young Jang, Gary D. Hachtel, Fabio Somenzi |
| 1996 | ISLPED | 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 |
| 1995 | DAC | 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 |
| 1995 | ICCAD | Boolean techniques for low power driven re-synthesis. | R. Iris Bahar, Fabio Somenzi |
| 1995 | ICCAD | Who are the variables in your neighborhood. | Shipra Panda, Fabio Somenzi |
| 1995 | ICCAD | High-density reachability analysis. | Kavita Ravi, Fabio Somenzi |
| 1995 | ISLPED | 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 |
| 1994 | DAC | Probabilistic Analysis of Large Finite State Machines. | Gary D. Hachtel, Enrico Macii, Abelardo Pardo, Fabio Somenzi |
| 1994 | ICCAD | A symbolic method to reduce power consumption of circuits containing false paths. | R. Iris Bahar, Gary D. Hachtel, Enrico Macii, Fabio Somenzi |
| 1994 | ICCAD | Re-encoding sequential circuits to reduce power dissipation. | Gary D. Hachtel, Mariano Hermida de la Rica, Abelardo Pardo, Massimo Poncino, Fabio Somenzi |
| 1994 | ICCAD | Symmetry detection and dynamic variable ordering of decision diagrams. | Shipra Panda, Fabio Somenzi, Bernard Plessier |
| 1994 | ICCD | A Structural Approach to State Space Decomposition for Approximate Reachability Analysis. | Hyunwoo Cho, Gary D. Hachtel, Enrico Macii, Massimo Poncino, Fabio Somenzi |
| 1993 | CAV | Automatic Generation of Network Invariants for the Verification of Iterative Sequential Systems. | June-Kyung Rho, Fabio Somenzi |
| 1993 | DAC | Algorithms for Approximate FSM Traversal. | Hyunwoo Cho, Gary D. Hachtel, Enrico Macii, Bernard Plessier, Fabio Somenzi |
| 1993 | DAC | Minimum Length Synchronizing Sequences of Finite State Machine. | June-Kyung Rho, Fabio Somenzi, Carl Pixley |
| 1993 | ICCAD | Algebraic decision diagrams and their applications. | R. Iris Bahar, Erica A. Frohm, Charles M. Gaona, Gary D. Hachtel, Enrico Macii, Abelardo Pardo, Fabio Somenzi |
| 1993 | ICCAD | A symbolic algorithm for maximum flow in 0-1 networks. | Gary D. Hachtel, Fabio Somenzi |
| 1992 | DAC | Inductive Verification of Iterative Systems. | June-Kyung Rho, Fabio Somenzi |
| 1992 | ICCAD | A new algorithm for the binate covering problem and its application to the minimization of Boolean relations. | Seh-Woong Jeong, Fabio Somenzi |
| 1992 | ICCAD | Verification of systems containing counters. | Enrico Macii, Bernard Plessier, Fabio Somenzi |
| 1992 | ICCD | The Role of Prime Compatibles in the Minimization of Finite State Machines. | June-Kyung Rho, Fabio Somenzi |
| 1991 | ICCAD | Extended BDD's: Trading off Canonicity for Structure in Verification Algorithms. | Seh-Woong Jeong, Bernard Plessier, Gary D. Hachtel, Fabio Somenzi |
| 1991 | ICCAD | Variable Ordering and Selection for FSM Traversal. | Seon-Woong Jeong, Bernard Plessier, Gary D. Hachtel, Fabio Somenzi |
| 1991 | ICCAD | Don't Care Sequences and the Optimization of Interacting Finite State Machines. | June-Kyung Rho, Gary D. Hachtel, Fabio Somenzi |
| 1991 | ICCD | Redundancy Identification and Removal Based on Implicit State Enumeration. | Hyunwoo Cho, Gary D. Hachtel, Fabio Somenzi |
| 1991 | ITC | Fast Sequential ATPG Based on Implicit State Enumeration. | Hyunwoo Cho, Gary D. Hachtel, Fabio Somenzi |
| 1990 | ICCAD | ATPG Aspects of FSM Verification. | Hyunwoo Cho, Gary D. Hachtel, Seh-Woong Jeong, Bernard Plessier, Eric M. Schwarz, Fabio Somenzi |
| 1990 | ICCAD | Minimization of Symbolic Relations. | Bill Lin, Fabio Somenzi |
| 1989 | ICCAD | An exact minimizer for Boolean relations. | Robert K. Brayton, Fabio Somenzi |
| 1988 | DAC | The Performance of the Concurrent Fault Simulation Algorithms in MOZART. | Silvano Gai, Pier Luca Montessoro, Fabio Somenzi |
| 1988 | ICCAD | Don't cares and global flow analysis of Boolean networks. | Robert K. Brayton, Ellen M. Sentovich, Fabio Somenzi |
| 1983 | DAC | A new integrated system for PLA testing and verification. | Fabio Somenzi, Silvano Gai, Marco Mezzalama, Paolo Prinetto |