BibSLEIGH — Randal_E

Travelled to:

1 × Belgium
1 × Canada
1 × Denmark
1 × Estonia
1 × Finland
1 × France
1 × Germany
1 × Israel
1 × Italy
1 × Spain
2 × Portugal
22 × USA

Collaborated with:

∅ M.N.Velev S.A.Seshia S.K.Lahiri D.L.Beatty A.Goel A.Jain C.B.McDonald Y.Chen M.Pandey C.H.Seger K.Cho K.S.Brace O.Strichman R.Raimi M.D.Schuster B.Cook G.Hasteer S.M.German K.L.Nelson S.Jain R.L.Rudell S.A.Kravitz R.A.Rutenbar K.Subramani M.Talupur B.Yang R.G.Simmons D.R.O'Hallaron M.S.Abadir V.Ganapathy S.Jha T.W.Reps T.J.Sheffler D.Kröning J.Ouaknine B.A.Brady H.Cui J.Simsa Y.Lin H.Li B.Blum X.Xu J.Yang G.A.Gibson

Talks about:

symbol (18) verif (17) use (14) formal (13) simul (13) circuit (10) function (9) boolean (9) model (8) level (8)

Person: Randal E. Bryant

DBLP: Bryant:Randal_E=

Facilitated 1 volumes:

Contributed to:

2013

2007

2006

2005

2004

2003

2002

2001

2000

1999

1998

1997

1996

1995

1994

1991

1990

1989

1988

1987

1985

1981

2007

Wrote 56 papers:

SOSP-2013-CuiSLLBXYGB #named #reliability #runtime #thread: Parrot: a practical runtime for deterministic, stable, and reliable threads (HC, JS, YHL, HL, BB, XX, JY, GAG, REB), pp. 388–405.
TACAS-2007-BryantKOSSB #abstraction: Deciding Bit-Vector Arithmetic with Abstraction (REB, DK, JO, SAS, OS, BAB), pp. 358–372.
LICS-2006-Bryant #infinity #using #verification: Formal Verification of Infinite State Systems Using Boolean Methods (REB), pp. 3–4.
RTA-2006-Bryant #infinity #using #verification: Formal Verification of Infinite State Systems Using Boolean Methods (REB), pp. 1–3.
CADE-2005-BryantS #verification: Decision Procedures Customized for Formal Verification (REB, SAS), pp. 255–259.
ICSE-2005-GanapathySJRB #automation: Automatic discovery of API-level exploits (VG, SAS, SJ, TWR, REB), pp. 312–321.
CAV-2004-GoelB #abstraction #functional #model checking #order #simulation: Symbolic Simulation, Model Checking and Abstraction with Partially Ordered Boolean Functional Vectors (AG, REB), pp. 255–267.
CAV-2004-LahiriB #bound #verification: Indexed Predicate Discovery for Unbounded System Verification (SKL, REB), pp. 135–147.
LICS-2004-SeshiaB #bound #quantifier #using: Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds (SAS, REB), pp. 100–109.
TACAS-2004-LahiriBGT #similarity: Revisiting Positive Equality (SKL, REB, AG, MT), pp. 1–15.
VMCAI-2004-LahiriB #abstraction #invariant #quantifier: Constructing Quantified Invariants via Predicate Abstraction (SKL, REB), pp. 267–281.
CAV-2003-LahiriB #deduction #verification: Deductive Verification of Advanced Out-of-Order Microprocessors (SKL, REB), pp. 341–353.
CAV-2003-LahiriBC #abstraction #approach: A Symbolic Approach to Predicate Abstraction (SKL, REB, BC), pp. 141–153.
CAV-2003-SeshiaB #automaton #bound #model checking #using: Unbounded, Fully Symbolic Model Checking of Timed Automata using Boolean Methods (SAS, REB), pp. 154–166.
DAC-2003-GoelHB #order #representation: Symbolic representation with ordered function templates (AG, GH, REB), pp. 431–435.
DAC-2003-SeshiaLB #hybrid #logic #satisfiability: A hybrid SAT-based decision procedure for separation logic with uninterpreted functions (SAS, SKL, REB), pp. 425–430.
DATE-2003-GoelB #analysis #functional #reachability #set: Set Manipulation with Boolean Functional Vectors for Symbolic Reachability Analysis (AG, REB), pp. 10816–10821.
CAV-2002-BryantLS #logic #modelling #using #verification: Modeling and Verifying Systems Using a Logic of Counter Arithmetic with λ Expressions and Uninterpreted Functions (REB, SKL, SAS), pp. 78–92.
CAV-2002-StrichmanSB #satisfiability: Deciding Separation Formulas with SAT (OS, SAS, REB), pp. 209–222.
CAV-2001-VelevB #logic #named #similarity: EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative Transformations (MNV, REB), pp. 235–240.
DAC-2001-McDonaldB #analysis #simulation #using: Computing Logic-Stage Delays Using Circuit Simulation and Symbolic Elmore Analysis (CBM, REB), pp. 283–288.
DAC-2001-VelevB #effectiveness #satisfiability #using #verification: Effective Use of Boolean Satisfiability Procedures in the Formal Verification of Superscalar and VLIW Microprocessors (MNV, REB), pp. 226–231.
CAV-2000-BryantV #constraints #satisfiability #transitive: Boolean Satisfiability with Transitivity Constraints (REB, MNV), pp. 85–98.
DAC-2000-McDonaldB #clustering #scheduling #simulation #using: Symbolic timing simulation using cluster scheduling (CBM, REB), pp. 254–259.
DAC-2000-VelevB #branch #exception #functional #multi #predict #verification: Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction (MNV, REB), pp. 112–117.
CAV-1999-BryantGV #logic #similarity: Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions (REB, SMG, MNV), pp. 470–482.
CAV-1999-YangSBO #constraints #model checking #modelling #optimisation: Optimizing Symbolic Model Checking for Constraint-Rich Models (BY, RGS, REB, DRO), pp. 328–340.
DAC-1999-VelevB #pipes and filters #similarity #verification: Exploiting Positive Equality and Partial Non-Consistency in the Formal Verification of Pipelined Microprocessors (MNV, REB), pp. 397–401.
CAV-1998-ChenB #float #verification: Verification of Floating-Point Adders (YAC, REB), pp. 488–499.
TACAS-1998-Bryant #pipes and filters #verification: Formal Verification of Pipelined Processors (REB), pp. 1–4.
TACAS-1998-VelevB #array #memory management #modelling #performance #simulation: Efficient Modeling of Memory Arrays in Symbolic Ternary Simulation (MNV, REB), pp. 136–150.
CAV-1997-PandeyB #evaluation #symmetry #verification: Exploiting Symmetry When Verifying Transitor-Level Circuits by Symbolic Trajectory Evaluation (MP, REB), pp. 244–255.
CAV-1997-VelevBJ #array #memory management #modelling #performance #simulation: Efficient Modeling of Memory Arrays in Symbolic Simulation (MNV, REB, AJ), pp. 388–399.
DAC-1997-NelsonJB #execution #verification: Formal Verification of a Superscalar Execution Unit (KLN, AJ, REB), pp. 161–166.
DAC-1997-PandeyRBA #evaluation #using #verification: Formal Verification of Content Addressable Memories Using Symbolic Trajectory Evaluation (MP, RR, REB, MSA), pp. 167–172.
DAC-1996-Bryant #analysis: Bit-Level Analysis of an SRT Divider Circuit (REB), pp. 661–665.
DAC-1996-PandeyRBB #array #evaluation #using #verification: Formal Verification of PowerPC Arrays Using Symbolic Trajectory Evaluation (MP, RR, DLB, REB), pp. 649–654.
CAV-1995-Bryant #multi #verification: Multipliers and Dividers: Insights on Arithmetic Circuits Verification (REB), pp. 1–3.
DAC-1995-BryantC #diagrams #verification: Verification of Arithmetic Circuits with Binary Moment Diagrams (REB, YAC), pp. 535–541.
DAC-1995-JainBJ #abstraction #automation: Automatic Clock Abstraction from Sequential Circuits (SJ, REB, AJ), pp. 707–711.
DAC-1994-BeattyB #simulation #using #verification: Formally Verifying a Microprocessor Using a Simulation Methodology (DLB, REB), pp. 596–602.
DAC-1991-BryantBS #evaluation #hardware #verification: Formal Hardware Verification by Symbolic Ternary Trajectory Evaluation (REB, DLB, CJHS), pp. 397–402.
DAC-1991-JainB #hardware #simulation: Mapping Switch-Level Simulation onto Gate-Level Hardware Accelerators (AJ, REB), pp. 219–222.
CAV-1990-BryantS #modelling #using #verification: Formal Verification of Digital Circuits Using Symbolic Ternary System Models (REB, CJHS), pp. 33–43.
DAC-1990-BraceRB #implementation #performance: Efficient Implementation of a BDD Package (KSB, RLR, REB), pp. 40–45.
DAC-1990-Bryant #simulation: Symbolic Simulation — Techniques and Applications (REB), pp. 517–521.
DAC-1989-ChoB #fault #generative #simulation: Test Pattern Generation for Sequential MOS Circuits by Symbolic Fault Simulation (KC, REB), pp. 418–423.
DAC-1989-KravitzBR #parallel #simulation: Massively Parallel Switch-Level Simulation: A Feasibility Study (SAK, REB, RAR), pp. 91–97.
DAC-1988-BeattyB #analysis #incremental #performance #using: Fast Incremental Circuit Analysis Using Extracted Hierarchy (DLB, REB), pp. 495–500.
DAC-1988-Bryant #design: CAD Tool Needs for System Designers (REB), p. 476.
DAC-1987-BryantBBCS #named: COSMOS: A Compiled Simulator for MOS Circuits (REB, DLB, KSB, KC, TJS), pp. 9–16.
DAC-1985-Bryant #representation #using #visual notation: Symbolic manipulation of Boolean functions using a graphical representation (REB), pp. 688–694.
DAC-1985-BryantS #concurrent #evaluation #fault #performance: Performance evaluation of FMOSSIM, a concurrent switch-level fault simulator (REB, MDS), pp. 715–719.
DAC-1981-Bryant #named: MOSSIM: A switch-level simulator for MOS LSI (REB), pp. 786–790.
SMT-J-2006-SeshiaSB #constraints #on the: On Solving Boolean Combinations of UTVPI Constraints (SAS, KS, REB), pp. 67–90.