Fabio Somenzi

ORCID

Publication Activity (10 Years)

Years Active: 1983-2024
Publications (10 Years): 40

Top Venues

Publications

Milad Kazemi, Mateo Perez, Fabio Somenzi, Sadegh Soudjani, Ashutosh Trivedi, Alvaro Velasquez
Assume-Guarantee Reinforcement Learning. AAAI (2024)
Mateo Perez, Fabio Somenzi, Ashutosh Trivedi
A PAC Learning Algorithm for LTL and Omega-Regular Objectives in MDPs. AAAI (2024)
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak
Omega-Regular Decision Processes. AAAI (2024)
Taylor Dohmen, Mateo Perez, Fabio Somenzi, Ashutosh Trivedi
Regular Reinforcement Learning. CAV (3) (2024)
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak
Multi-objective ω-Regular Reinforcement Learning. Formal Aspects Comput. 35 (2) (2023)
Rajeev Alur, Osbert Bastani, Kishor Jothimurugan, Mateo Perez, Fabio Somenzi, Ashutosh Trivedi
Policy Synthesis and Reinforcement Learning for Discounted LTL. CAV (1) (2023)
Rajeev Alur, Osbert Bastani, Kishor Jothimurugan, Mateo Perez, Fabio Somenzi, Ashutosh Trivedi
Policy Synthesis and Reinforcement Learning for Discounted LTL. CoRR (2023)
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak
Omega-Regular Decision Processes. CoRR (2023)
Mateo Perez, Fabio Somenzi, Ashutosh Trivedi
A PAC Learning Algorithm for LTL and Omega-regular Objectives in MDPs. CoRR (2023)
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak
Mungojerrie: Linear-Time Objectives in Model-Free Reinforcement Learning. TACAS (1) (2023)
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak
Omega-Regular Reward Machines. ECAI (2023)
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak
Omega-Regular Reward Machines. CoRR (2023)
Milad Kazemi, Mateo Perez, Fabio Somenzi, Sadegh Soudjani, Ashutosh Trivedi, Alvaro Velasquez
Assume-Guarantee Reinforcement Learning. CoRR (2023)
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak
Alternating Good-for-MDP Automata. CoRR (2022)
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak
Recursive Reinforcement Learning. CoRR (2022)
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak
An Impossibility Result in Automata-Theoretic Reinforcement Learning. ATVA (2022)
Abolfazl Lavaei, Mateo Perez, Milad Kazemi, Fabio Somenzi, Sadegh Soudjani, Ashutosh Trivedi, Majid Zamani
Compositional Reinforcement Learning for Discrete-Time Stochastic Control Systems. CoRR (2022)
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak
Reinforcement Learning with Guarantees that Hold for Ever. FMICS (2022)
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak
Recursive Reinforcement Learning. NeurIPS (2022)
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak
Alternating Good-for-MDPs Automata. ATVA (2022)
Milad Kazemi, Mateo Perez, Fabio Somenzi, Sadegh Soudjani, Ashutosh Trivedi, Alvaro Velasquez
Translating Omega-Regular Specifications to Average Objectives for Model-Free Reinforcement Learning. AAMAS (2022)
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak
Model-Free Reinforcement Learning for Lexicographic Omega-Regular Objectives. FM (2021)
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak
Model-free Reinforcement Learning for Branching Markov Decision Processes. CoRR (2021)
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak
Mungojerrie: Reinforcement Learning of Linear-Time Objectives. CoRR (2021)
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak
Model-Free Reinforcement Learning for Branching Markov Decision Processes. CAV (2) (2021)
Abolfazl Lavaei, Fabio Somenzi, Sadegh Soudjani, Ashutosh Trivedi, Majid Zamani
Formal Controller Synthesis for Continuous-Space MDPs via Model-Free Reinforcement Learning. ICCPS (2020)
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak
Reward Shaping for Reinforcement Learning with Omega-Regular Objectives. CoRR (2020)
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak
Faithful and Effective Reward Schemes for Model-Free Reinforcement Learning of Omega-Regular Objectives. ATVA (2020)
Abolfazl Lavaei, Fabio Somenzi, Sadegh Soudjani, Ashutosh Trivedi, Majid Zamani
Formal Controller Synthesis for Continuous-Space MDPs via Model-Free Reinforcement Learning. CoRR (2020)
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak
Model-Free Reinforcement Learning for Stochastic Parity Games. CONCUR (2020)
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak
Good-for-MDPs Automata for Probabilistic Analysis and Reinforcement Learning. TACAS (1) (2020)
Ernst Moritz Hahn, Mateo Perez, Fabio Somenzi, Ashutosh Trivedi, Sven Schewe, Dominik Wojtczak
Good-for-MDPs Automata. CoRR (2019)
Fabio Somenzi, Ashutosh Trivedi
Reinforcement Learning and Formal Requirements. NSV@CAV (2019)
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak
Omega-Regular Objectives in Model-Free Reinforcement Learning. TACAS (1) (2019)
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak
Limit reachability for model-free reinforcement learning of ω-regular objectives. SNR (2019)
Fabio Somenzi, Behrouz Touri, Ashutosh Trivedi
Global Almost-Sure Reachability in Stochastic Constant-Rate Multi-Mode Systems. HSCC (2018)
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak
Omega-Regular Objectives in Model-Free Reinforcement Learning. CoRR (2018)
Shankara Narayanan Krishna, Aviral Kumar, Fabio Somenzi, Behrouz Touri, Ashutosh Trivedi
The Reach-Avoid Problem for Constant-Rate Multi-Mode Systems. CoRR (2017)
Shankara Narayanan Krishna, Aviral Kumar, Fabio Somenzi, Behrouz Touri, Ashutosh Trivedi
The Reach-Avoid Problem for Constant-Rate Multi-mode Systems. ATVA (2017)
Michael Dooley, Fabio Somenzi
Proving Parameterized Systems Safe by Generalizing Clausal Proofs of Small Instances. CAV (1) (2016)
Yan Zhang, Sriram Sankaranarayanan, Fabio Somenzi
Sparse statistical model inference for analog circuits under process variations. ASP-DAC (2014)
Yan Zhang, Sriram Sankaranarayanan, Fabio Somenzi
Statistically Sound Verification and Optimization for Complex Systems. ATVA (2014)
Zyad Hassan, Aaron R. Bradley, Fabio Somenzi
Better generalization in IC3. FMCAD (2013)
Kuntal Nanshi, Fabio Somenzi
Using Abstraction to Guide the Search for Long Error Traces. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 32 (3) (2013)
Saqib Sohail, Fabio Somenzi
Efficient handling of obligation constraints in synthesis from omega-regular specifications. FMCAD (2013)
Saqib Sohail, Fabio Somenzi
Safety first: a two-stage algorithm for the synthesis of reactive systems. Int. J. Softw. Tools Technol. Transf. 15 (5-6) (2013)
Yan Zhang, Sriram Sankaranarayanan, Fabio Somenzi, Xin Chen, Erika Ábrahám
From statistical model checking to statistical model inference: characterizing the effect of process variations in analog circuits. ICCAD (2013)
Zyad Hassan, Aaron R. Bradley, Fabio Somenzi
Incremental, Inductive CTL Model Checking. CAV (2012)
Yan Zhang, Sriram Sankaranarayanan, Fabio Somenzi
Piecewise linear modeling of nonlinear devices for formal verification of analog circuits. FMCAD (2012)
Aaron R. Bradley, Fabio Somenzi, Zyad Hassan, Yan Zhang
An incremental approach to model checking progress properties. FMCAD (2011)
HyoJung Han, HoonSang Jin, Fabio Somenzi
Clause simplification through dominator analysis. DATE (2011)
Zyad Hassan, Yan Zhang, Fabio Somenzi
A Study of Sweeping Algorithms in the Context of Model Checking. DIFTS@FMCAD (2011)
Fabio Somenzi, Aaron R. Bradley
IC3: where monolithic and incremental meet. FMCAD (2011)
HyoJung Han, Fabio Somenzi, HoonSang Jin
Making Deduction More Effective in SAT Solvers. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 29 (8) (2010)
Kuntal Nanshi, Fabio Somenzi
Constraints in one-to-many concretization for abstraction refinement. DAC (2009)
HyoJung Han, Fabio Somenzi
On-the-Fly Clause Improvement. SAT (2009)
Hyondeuk Kim, Fabio Somenzi, HoonSang Jin
Efficient Term-ITE Conversion for Satisfiability Modulo Theories. SAT (2009)
Saqib Sohail, Fabio Somenzi
Safety first: A two-stage algorithm for LTL games. FMCAD (2009)
Kuntal Nanshi, Fabio Somenzi
Improved Visibility in One-to-Many Trace Concretization. DATE (2008)
Saqib Sohail, Fabio Somenzi, Kavita Ravi
A Hybrid Algorithm for LTL Games. VMCAI (2008)
Hyondeuk Kim, HoonSang Jin, Kavita Ravi, Petr Spacek, John Pierce, Robert P. Kurshan, Fabio Somenzi
Application of Formal Word-Level Analysis to Constrained Random Simulation. CAV (2008)
Roderick Bloem, Marco Roveri, Fabio Somenzi
Preface. Electron. Notes Theor. Comput. Sci. 174 (4) (2007)
Hyondeuk Kim, HoonSang Jin, Fabio Somenzi
Disequality Management in Integer Difference Logic via Finite Instantiations. J. Satisf. Boolean Model. Comput. 3 (1-2) (2007)
HyoJung Han, Fabio Somenzi
Alembic: An Efficient Algorithm for CNF Preprocessing. DAC (2007)
David Ward, Fabio Somenzi
Decomposing image computation for symbolic reachability analysis using control flow information. ICCAD (2006)
Bing Li, Fabio Somenzi
Efficient Abstraction Refinement in Interpolation-Based Unbounded Model Checking. TACAS (2006)
Chao Wang, Roderick Bloem, Gary D. Hachtel, Kavita Ravi, Fabio Somenzi
Compositional SCC Analysis for Language Emptiness. Formal Methods Syst. Des. 28 (1) (2006)
Hyondeuk Kim, Fabio Somenzi
Finite Instantiations for Integer Difference Logic. FMCAD (2006)
Mohammad Awedh, Fabio Somenzi
Termination Criteria for Bounded Model Checking: Extensions and Comparison. Electron. Notes Theor. Comput. Sci. 144 (1) (2006)
Roderick Bloem, Harold N. Gabow, Fabio Somenzi
Symbolic Steps. Formal Methods Syst. Des. 28 (1) (2006)
Chao Wang, Bing Li, HoonSang Jin, Gary D. Hachtel, Fabio Somenzi
Improving Ariadne's Bundle by Following Multiple Threads in Abstraction Refinement. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 25 (11) (2006)
Kuntal Nanshi, Fabio Somenzi
Guiding simulation with increasingly refined abstract traces. DAC (2006)
HoonSang Jin, Fabio Somenzi
Strong conflict analysis for propositional satisfiability. DATE (2006)
Mohammad Awedh, Fabio Somenzi
Automatic invariant strengthening to prove properties in bounded model checking. DAC (2006)
HoonSang Jin, Fabio Somenzi
An Incremental Algorithm to Check Satisfiability for Bounded Model Checking. Electron. Notes Theor. Comput. Sci. 119 (2) (2005)
HoonSang Jin, Fabio Somenzi
Prime clauses for fast enumeration of satisfying assignments to boolean circuits. DAC (2005)
David Ward, Fabio Somenzi
Automatic Generation of Hints for Symbolic Traversal. CHARME (2005)
HoonSang Jin, HyoJung Han, Fabio Somenzi
Efficient Conflict Analysis for Finding All Satisfying Assignments of a Boolean Circuit. TACAS (2005)
Bing Li, Chao Wang, Fabio Somenzi
Abstraction refinement in symbolic model checking using satisfiability as the only decision procedure. Int. J. Softw. Tools Technol. Transf. 7 (2) (2005)
Chao Wang, HoonSang Jin, Gary D. Hachtel, Fabio Somenzi
Refining the SAT decision ordering for bounded model checking. DAC (2004)
HoonSang Jin, Mohammad Awedh, Fabio Somenzi
CirCUs: A Satisfiability Solver Geared towards Bounded Model Checking. CAV (2004)
Chao Wang, Gary D. Hachtel, Fabio Somenzi
Fine-Grain Abstraction and Sequential Don't Cares for Large Scale Model Checking. ICCD (2004)
HoonSang Jin, Fabio Somenzi
CirCUs: A Hybrid Satisfiability Solver. SAT (2004)
Mohammad Awedh, Fabio Somenzi
Proving More Properties with Bounded Model Checking. CAV (2004)
HoonSang Jin, Fabio Somenzi
CirCUs: A Hybrid Satisfiability Solver. SAT (Selected Papers (2004)
HoonSang Jin, Kavita Ravi, Fabio Somenzi
Fate and free will in error traces. Int. J. Softw. Tools Technol. Transf. 6 (2) (2004)
Mohammad Awedh, Fabio Somenzi
Increasing the Robustness of Bounded Model Checking by Computing Lower Bounds on the Reachable States. FMCAD (2004)
Bing Li, Fabio Somenzi
Efficient computation of small abstraction refinements. ICCAD (2004)
Kavita Ravi, Fabio Somenzi
Minimal Assignments for Bounded Model Checking. TACAS (2004)
Rajesh K. Gupta, Shishpal Rawat, Sandeep K. Shukla, Brian Bailey, Daniel K. Beece, Masahiro Fujita, Carl Pixley, John O'Leary, Fabio Somenzi
Formal verification - prove it or pitch it. DAC (2003)
Fabio Somenzi
The Charme of Abstract Entities. CHARME (2003)
Chao Wang, Gary D. Hachtel, Fabio Somenzi
The Compositional Far Side of Image Computation. ICCAD (2003)
Sankar Gurumurthy, Orna Kupferman, Fabio Somenzi, Moshe Y. Vardi
On Complementing Nondeterministic Büchi Automata. CHARME (2003)
Bing Li, Chao Wang, Fabio Somenzi
A satisfiability-based approach to abstraction refinement in model checking. Electron. Notes Theor. Comput. Sci. 89 (4) (2003)
Chao Wang, Bing Li, HoonSang Jin, Gary D. Hachtel, Fabio Somenzi
Improving Ariadneýs Bundle by Following Multiple Threads in Abstraction Refinement. ICCAD (2003)
Nikhil Jayakumar, Mitra Purandare, Fabio Somenzi
Dos and don'ts of CTL state coverage estimation. DAC (2003)
Sankar Gurumurthy, Roderick Bloem, Fabio Somenzi
Fair Simulation Minimization. CAV (2002)
Fabio Somenzi, Kavita Ravi, Roderick Bloem
Analysis of Symbolic SCC Hull Algorithms. FMCAD (2002)
HoonSang Jin, Kavita Ravi, Fabio Somenzi
Fate and Free Will in Error Traces. TACAS (2002)
HoonSang Jin, Andreas Kuehlmann, Fabio Somenzi
Fine-Grain Conjunction Scheduling for Symbolic Reachability Analysis. TACAS (2002)

Fabio Somenzi.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Fabio Somenzi