BibSLEIGH — Fabio

Travelled to:

1 × Austria
1 × Denmark
1 × Greece
1 × Italy
1 × Spain
2 × Canada
2 × United Kingdom
21 × USA
3 × Germany
4 × France

Collaborated with:

H.Jin K.Ravi E.Macii H.Han G.D.Hachtel K.Nanshi R.Bloem M.Awedh J.Rho M.Purandare H.Kim B.Kumthekar A.Pardo H.Cho S.Gai B.Li M.Dooley S.Manne C.Pixley R.I.Bahar M.Poncino Z.Hassan A.R.Bradley S.Sohail N.Jayakumar S.Gurumurthy A.Kuehlmann G.Cabodi S.Quer M.Pedram D.Grunwald C.Meinel T.Theobald P.L.Montessoro R.K.Ranjan R.K.Brayton T.R.Shiple C.Wang I.Moon J.H.Kukula V.Singhal L.Benini K.L.McMillan M.Mezzalama P.Prinetto B.Plessier P.Spacek J.Pierce R.P.Kurshan R.K.Gupta S.Rawat S.K.Shukla B.Bailey D.K.Beece M.Fujita J.O'Leary A.L.Sangiovanni-Vincentelli A.Aziz S.Cheng S.A.Edwards S.P.Khatri Y.Kukimoto S.Qadeer S.Sarwary G.Swamy T.Villa

Talks about:

model (10) check (9) satisfi (7) analysi (7) verif (7) algorithm (6) effici (6) state (6) circuit (5) system (5)

Person: Fabio Somenzi

DBLP: Somenzi:Fabio

Facilitated 1 volumes:

Contributed to:

2012

2011

2009

2008

2007

2006

2005

2004

2005

2004

2003

2002

2000

1999

1998

1997

1996

1995

1994

1993

1992

1988

1983

2016

2007

Wrote 54 papers:

CAV-2012-HassanBS #incremental #induction #model checking: Incremental, Inductive CTL Model Checking (ZH, ARB, FS), pp. 532–547.
DATE-2011-HanJS #analysis: Clause simplification through dominator analysis (HH, HJ, FS), pp. 143–148.
DAC-2009-NanshiS #abstraction #constraints #refinement: Constraints in one-to-many concretization for abstraction refinement (KN, FS), pp. 569–574.
SAT-2009-HanS #on the fly: On-the-Fly Clause Improvement (HH, FS), pp. 209–222.
SAT-2009-KimSJ #modulo theories #performance #satisfiability: Efficient Term-ITE Conversion for Satisfiability Modulo Theories (HK, FS, HJ), pp. 195–208.
CAV-2008-KimJRSPKS #analysis #random #simulation: Application of Formal Word-Level Analysis to Constrained Random Simulation (HK, HJ, KR, PS, JP, RPK, FS), pp. 487–490.
DATE-2008-NanshiS: Improved Visibility in One-to-Many Trace Concretization (KN, FS), pp. 819–824.
VMCAI-2008-SohailSR #algorithm #game studies #hybrid #ltl: A Hybrid Algorithm for LTL Games (SS, FS, KR), pp. 309–323.
DAC-2007-HanS #algorithm #named #performance #preprocessor: Alembic: An Efficient Algorithm for CNF Preprocessing (HH, FS), pp. 582–587.
DAC-2006-AwedhS #automation #bound #invariant #model checking: Automatic invariant strengthening to prove properties in bounded model checking (MA, FS), pp. 1073–1076.
DAC-2006-NanshiS #simulation: Guiding simulation with increasingly refined abstract traces (KN, FS), pp. 737–742.
DATE-2006-JinS #analysis #satisfiability: Strong conflict analysis for propositional satisfiability (HJ, FS), pp. 818–823.
TACAS-2006-LiS #abstraction #bound #model checking #performance #refinement: Efficient Abstraction Refinement in Interpolation-Based Unbounded Model Checking (BL, FS), pp. 227–241.
DAC-2005-JinS #performance: Prime clauses for fast enumeration of satisfying assignments to boolean circuits (HJ, FS), pp. 750–753.
TACAS-2005-JinHS #analysis #performance: Efficient Conflict Analysis for Finding All Satisfying Assignments of a Boolean Circuit (HJ, HH, FS), pp. 287–300.
CAV-2004-AwedhS #bound #model checking #proving: Proving More Properties with Bounded Model Checking (MA, FS), pp. 96–108.
CAV-2004-JinAS #bound #model checking #named #satisfiability #towards: CirCUs: A Satisfiability Solver Geared towards Bounded Model Checking (HJ, MA, FS), pp. 519–522.
DAC-2004-WangJHS #bound #model checking #satisfiability: Refining the SAT decision ordering for bounded model checking (CW, HJ, GDH, FS), pp. 535–538.
SAT-2004-JinS #hybrid #named #satisfiability: CirCUs: A Hybrid Satisfiability Solver (HJ, FS), pp. 47–55.
SAT-J-2004-JinS05 #hybrid #named #satisfiability: CirCUs: A Hybrid Satisfiability Solver (HJ, FS), pp. 211–223.
TACAS-2004-RaviS #bound #model checking: Minimal Assignments for Bounded Model Checking (KR, FS), pp. 31–45.
DAC-2003-GuptaRSBBFPOS #verification: Formal verification — prove it or pitch it (RKG, SR, SKS, BB, DKB, MF, CP, JO, FS), pp. 710–711.
DAC-2003-JayakumarPS #estimation: Dos and don’ts of CTL state coverage estimation (NJ, MP, FS), pp. 292–295.
CAV-2002-GurumurthyBS #simulation: Fair Simulation Minimization (SG, RB, FS), pp. 610–624.
CAV-2002-PurandareS: Vacuum Cleaning CTL Formulae (MP, FS), pp. 485–499.
TACAS-2002-JinKS #analysis #reachability #scheduling: Fine-Grain Conjunction Scheduling for Symbolic Reachability Analysis (HJ, AK, FS), pp. 312–326.
TACAS-2002-JinRS #fault: Fate and Free Will in Error Traces (HJ, KR, FS), pp. 445–459.
CAV-2000-SomenziB #automaton #ltl #performance: Efficient Büchi Automata from LTL Formulae (FS, RB), pp. 248–263.
DAC-2000-BloemRS #model checking: Symbolic guided search for CTL model checking (RB, KR, FS), pp. 29–34.
DAC-2000-CabodiQS #optimisation #verification: Optimizing sequential verification by retiming transformations (GC, SQ, FS), pp. 601–606.
DAC-2000-MoonKRS #image: To split or to conjoin: the question in image computation (IHM, JHK, KR, FS), pp. 23–28.
DATE-2000-KumthekarS #logic #optimisation #reduction: Power and Delay Reduction via Simultaneous Logic and Placement Optimization in FPGAs (BK, FS), pp. 202–207.
CAV-1999-BloemRS #linear #logic #model checking #performance: Efficient Decision Procedures for Model Checking of Linear Time Logic Properties (RB, KR, FS), pp. 222–235.
DATE-1999-RanjanSSB #using #verification: Using Combinational Verification for Sequential Circuits (RKR, VS, FS, RKB), pp. 138–144.
DAC-1998-KumthekarBMS #optimisation: In-Place Power Optimization for LUT-Based FPGAs (BK, LB, EM, FS), pp. 718–721.
DAC-1998-RaviMSS #approximate #composition #diagrams: Approximation and Decomposition of Binary Decision Diagrams (KR, KLM, TRS, FS), pp. 445–450.
DAC-1997-MaciiPS #estimation #modelling #optimisation: High-Level Power Modeling, Estimation, and Optimization (EM, MP, FS), pp. 504–511.
DAC-1997-ManneGS #locality #memory management: Remembrance of Things Past: Locality and Memory in BDDs (SM, DG, FS), pp. 196–201.
DAC-1997-MeinelST #diagrams #linear: Linear Sifting of Decision Diagrams (CM, FS, TT), pp. 202–207.
CAV-1996-BraytonHSSACEKKPQRSSSV #named #synthesis #verification: VIS: A System for Verification and Synthesis (RKB, GDH, ALSV, FS, AA, STC, SAE, SPK, YK, AP, SQ, RKR, SS, TRS, GS, TV), pp. 428–432.
DAC-1995-MannePBHSMP: Computing the Maximum Power Cycles of a Sequential Circuit (SM, AP, RIB, GDH, FS, EM, MP), pp. 23–28.
DAC-1994-HachtelMPS #analysis #finite #probability #scalability #state machine: Probabilistic Analysis of Large Finite State Machines (GDH, EM, AP, FS), pp. 270–275.
EDAC-1994-BaharCHMS #analysis #using: Timing Analysis of Combinational Circuits using ADD’s (RIB, HC, GDH, EM, FS), pp. 625–629.
EDAC-1994-ChoHMPS #algorithm #approximate #automaton #composition #traversal: A State Space Decomposition Algorithm for Approximate FSM Traversal (HC, GDH, EM, MP, FS), pp. 137–141.
EDAC-1994-HachtelMPS #algorithm #finite #state machine: Symbolic Algorithms to Calculate Steady-State Probabilities of a Finite State Machine (GDH, EM, AP, FS), pp. 214–218.
CAV-1993-RhoS #automation #generative #invariant #network #verification: Automatic Generation of Network Invariants for the Verification of Iterative Sequential Systems (JKR, FS), pp. 123–137.
DAC-1993-ChoHMPS #algorithm #approximate #automaton #traversal: Algorithms for Approximate FSM Traversal (HC, GDH, EM, BP, FS), pp. 25–30.
DAC-1993-RhoSP #finite #sequence #state machine: Minimum Length Synchronizing Sequences of Finite State Machine (JKR, FS, CP), pp. 463–468.
DAC-1992-RhoS #induction #verification: Inductive Verification of Iterative Systems (JKR, FS), pp. 628–633.
DAC-1988-GaiMS #algorithm #concurrent #fault #performance #simulation: The Performance of the Concurrent Fault Simulation Algorithms in MOZART (SG, PLM, FS), pp. 692–697.
DAC-1983-SomenziGMP #testing #verification: A new integrated system for PLA testing and verification (FS, SG, MM, PP), pp. 57–63.
CAV-2016-DooleyS #proving: Proving Parameterized Systems Safe by Generalizing Clausal Proofs of Small Instances (MD, FS), pp. 292–309.
SMT-J-2006-KimJS #difference #finite #integer #logic: Disequality Management in Integer Difference Logic via Finite Instantiations (HK, HJ, FS), pp. 47–66.