Travelled to:1 × Canada
1 × France
1 × Greece
1 × Italy
15 × USA
2 × Denmark
2 × United Kingdom
4 × Germany
Collaborated with:D.L.Dill J.D.Bingham Z.Rakamaric D.Babic F.M.d.Paula X.Feng S.P.Rajan A.Nahir M.T.Oliveira S.Bayless D.W.Currie M.Fujita G.York H.Wong-Toi T.Klenze B.Cook S.G.Govindaraju M.Horowitz A.J.Drexler C.H.Yang A.Ziv Z.Nevo A.Orni A.Condon S.Qadeer Z.Zhang M.R.Marty M.D.Hill M.M.K.Martin D.A.Wood F.Bacchini T.Fitzpatrick R.Ranjan D.Lacey M.Tan A.Piziali R.Galivanche M.Abramovici A.Camilleri B.Bentley H.Foster V.Bertacco S.Kapoor J.Backes C.Dodge A.Gacek T.Kahsai B.Kocik E.Kotelnikov J.Kukovec S.McLaughlin J.R.0004 N.Rungta J.Sizemore M.A.Stalzer P.Srinivasan P.Subotic C.Varming B.Whaley
Talks about:verif (13) automat (5) formal (5) use (5) effici (4) level (4) bdds (4) abstract (3) softwar (3) silicon (3)
Person: Alan J. Hu
DBLP: Hu:Alan_J=
Facilitated 1 volumes:
EdContributed to:
2012
20112010
2009
2008
200820072007
20072007200620062005
2005
2005200420022002
200220001998
19981994199319931992199120162019Wrote 31 papers:
- CAV-2012-PaulaHN #debugging #named #nondeterminism
- nuTAB-BackSpace: Rewriting to Normalize Non-determinism in Post-silicon Debug Traces (FMdP, AJH, AN), pp. 513–531.
- DAC-2011-PaulaNNOH #named
- TAB-BackSpace: unlimited-length trace buffers with zero additional on-chip overhead (FMdP, AN, ZN, AO, AJH), pp. 411–416.
- DAC-2010-NahirZGHACBFBK #validation #verification
- Bridging pre-silicon verification and post-silicon validation (AN, AZ, RG, AJH, MA, AC, BB, HF, VB, SK), pp. 94–95.
- VMCAI-2009-RakamaricH #low level #memory management #scalability
- A Scalable Memory Model for Low-Level Code (ZR, AJH), pp. 290–304.
- ASE-2008-RakamaricH #automation #axiom #static analysis #using
- Automatic Inference of Frame Axioms Using Static Analysis (ZR, AJH), pp. 89–98.
- ICSE-2008-BabicH #named #precise #scalability #static analysis
- Calysto: scalable and precise extended static checking (DB, AJH), pp. 211–220.
- CAV-2007-BabicH #abstraction #verification
- Structural Abstraction of Software Verification Conditions (DB, AJH), pp. 366–378.
- DAC-2007-BacchiniHFRLTPZ #question #verification
- Verification Coverage: When is Enough, Enough? (FB, AJH, TF, RR, DL, MT, AP, AZ), pp. 744–745.
- DAC-2007-PaulaH #effectiveness #simulation
- An Effective Guidance Strategy for Abstraction-Guided Simulation (FMdP, AJH), pp. 63–68.
- SEFM-2007-BabicHRC #proving #termination
- Proving Termination by Divergence (DB, AJH, ZR, BC), pp. 93–102.
- VMCAI-2007-RakamaricBH #data type #source code #verification
- An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures (ZR, JDB, AJH), pp. 106–121.
- CAV-2006-PaulaH #flexibility #framework #named #platform #simulation
- EverLost: A Flexible Platform for Industrial-Strength Abstraction-Guided Simulation (FMdP, AJH), pp. 282–285.
- DAC-2006-FengH #equivalence #verification
- Early cutpoint insertion for high-level software vs. RTL formal combinational equivalence verification (XF, AJH), pp. 1063–1068.
- DAC-2005-BabicBH #performance #satisfiability
- Efficient SAT solving: beyond supercubes (DB, JDB, AJH), pp. 744–749.
- HPCA-2005-MartyBHHMW #multi #using
- Improving Multiple-CMP Systems Using Token Coherence (MRM, JDB, MDH, AJH, MMKM, DAW), pp. 328–339.
- TACAS-2005-BinghamH #empirical #infinity #performance #verification
- Empirically Efficient Verification for a Class of Infinite-State Systems (JDB, AJH), pp. 77–92.
- CAV-2004-BinghamCHQZ #automation #bound #consistency #verification
- Automatic Verification of Sequential Consistency for Unbounded Addresses and Data Values (JDB, AC, AJH, SQ, ZZ), pp. 427–439.
- CAV-2002-BinghamH #bound #model checking
- Semi-formal Bounded Model Checking (JDB, AJH), pp. 280–294.
- DAC-2002-OliveiraH #automation #generative #interface #monitoring #specification
- High-Level specification and automatic generation of IP interface monitors (MTO, AJH), pp. 129–134.
- LCTES-SCOPES-2002-FengH #automation #verification
- Automatic formal verification for scheduled VLIW code (XF, AJH), pp. 85–92.
- DAC-2000-CurrieHR #automation #verification
- Automatic formal verification of DSP software (DWC, AJH, SPR), pp. 130–135.
- DAC-1998-GovindarajuDHH #approximate #reachability #using
- Approximate Reachability with BDDs Using Overlapping Projections (SGG, DLD, AJH, MH), pp. 451–456.
- FM-1998-FujitaRH #case study #experience #parallel #protocol #verification
- Two Real Formal Verification Experiences: ATM Switch Chip and Parallel Cache Protocol (MF, SPR, AJH), pp. 281–295.
- DAC-1994-HuYD #performance #verification
- New Techniques for Efficient Verification with Implicitly Conjoined BDDs (AJH, GY, DLD), pp. 276–282.
- CAV-1993-HuD #invariant #performance #using #verification
- Efficient Verification with BDDs using Implicitly Conjoined Invariants (AJH, DLD), pp. 3–14.
- DAC-1993-HuD #dependence #functional
- Reducing BDD Size by Exploiting Functional Dependencies (AJH, DLD), pp. 266–271.
- CAV-1992-HuDDY #specification #verification
- Higher-Level Specification and Verification with BDDs (AJH, DLD, AJD, CHY), pp. 82–95.
- CAV-1991-DillHW #simulation #using
- Checking for Language Inclusion Using Simulation Preorders (DLD, AJH, HWT), pp. 255–265.
- CAV-2016-KlenzeBH #flexibility #performance #smt #synthesis
- Fast, Flexible, and Minimal CTL Synthesis via SMT (TK, SB, AJH), pp. 136–156.
- CAV-2019-BackesBCDGHKKKK #analysis #network #reachability
- Reachability Analysis for AWS-Based Networks (JB, SB, BC, CD, AG, AJH, TK, BK, EK, JK, SM, JR0, NR, JS, MAS, PS, PS, CV, BW), pp. 231–241.