BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
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 DBLP: Somenzi:Fabio

Facilitated 1 volumes:

CAV 2003Ed

Contributed to:

CAV 20122012
DATE 20112011
DAC 20092009
SAT 20092009
CAV 20082008
DATE 20082008
VMCAI 20082008
DAC 20072007
DAC 20062006
DATE 20062006
TACAS 20062006
DAC 20052005
TACAS 20052005
CAV 20042004
DAC 20042004
SAT 20042004
SAT 20042005
TACAS 20042004
DAC 20032003
CAV 20022002
TACAS 20022002
CAV 20002000
DAC 20002000
DATE 20002000
CAV 19991999
DATE 19991999
DAC 19981998
DAC 19971997
CAV 19961996
DAC 19951995
DAC 19941994
EDAC-ETC-EUROASIC 19941994
CAV 19931993
DAC 19931993
DAC 19921992
DAC 19881988
DAC 19831983
CAV (1) 20162016
SMT 20062007

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.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.