Randal E. Bryant, Selected Presentations

• Modeling Data in Formal Verification: Bits, Bit Vectors, or Words . Invited tutorial at Formal Methods in Computer-Aided Design Austin, TX, November, 2007. Modified version at VLSI Design and Test, Taiwan, 2008.
• Data-Intensive Super Computing. Two versions:
  • Original . Presented in conjunction with the 2007 Federated Computing Research Conference.
  • Revised . Includes additions and refinements based on follow-up presentations.
• Bit-Vector Decision Procedures: A Basis for Reasoning about Hardware and Software
• System Modeling and Formal Verification with UCLID Keynote presentation, Haifa Verification Conference, Haifa, Israel.
• A View from the Engine Room: Computational Support for Symbolic Model Checking , 25 Years of Model Checking Workshop, Federated Logic Conference (FLoC), August, 2006.
• Formal Verification of Infinite-State Systems using Boolean Methods , Plenary Talk, Federated Logic Conference (FLoC), August, 2006.
• Introducing Computer Systems from a Programmer's Perspective , May, 2006.
• Computer Science Foundations for PhD Students, a Carnegie Mellon Perspective US-China Computer Science Leadership Summit, Beijing, May 23, 2006.
• Formal Verification of Infinite-State Systems using Boolean Methods
  Distinguished Lecture, MIT Computer Science and AI Laboratory, February, 2006.
• Decision Procedures Customized for Formal Verification
  Keynote Presentation, Conference on Automated Deduction (CADE 2005), July, 2005.
• Presentations at Intel, Haifa, Israel, July 2005:
  • SAT-based decision procedures for linear arithmetic and uninterpreted functions
  • System Modeling and Verification with UCLID
  • Symbolic Approaches to Invariant Checking and Automatic Predicate Abstraction
• Symbolic, Word-Level Hardware Verification
  Embedded Tutorial, International Conference on Computer-Aided Design (ICCAD '04), November, 2004.
• System Modeling and Verification with UCLID
  Keynote Presentation, MemoCODE 2004, June, 2004.
• SAT-Based Decision Procedures for Subsets of First-Order Logic
  • Part I: Equality with Uninterpreted Functions
  • Part II: Separation Logic
• Convergence Testing in Term-Level Bounded Model Checking
  Correct Hardware Design and Verification Methods (Charme '03), November, 2003.
• Formal Verification of Infinite-State Systems using Boolean Methods
  Distinguished Lecture, University of Pennsylvania Computer Science Department, October, 2003.
• Deductive Verification of Advanced Out-of-Order Microprocessors
  Computer-Aided Verification (CAV '03), July, 2003.
• Unbounded, Fully Symbolic Model Checking of Timed Automata using Boolean Methods
  Computer-Aided Verification (CAV '03), July, 2003.
• A Hybrid SAT-Based Decision Procedure for Separation Logic and Uninterpreted Functions
  Design Automation Conference (DAC '03), June, 2003.
• Formal Verification Using Infinite-State Models
  Distinguished Lecture, UCLA Computer Science Department, March, 2003.
• Symbolic Simulation and its Connection to Formal Verification
  Invited talk, Formal Methods in Computer-Aided Design, November, 2002.
• Modeling and Verification of Out-of-Order Processors in UCLID
  Formal Methods in Computer-Aided Design, November, 2002.
• Modeling and Verifying Systems using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions
  Computer-Aided Verification (CAV '02), July, 2002.
• Deciding Separation Formulas with SAT
  Computer-Aided Verification (CAV '02), July, 2002.
• Boolean Satisfiability with Transitivity Constraints
  Computer-Aided Verification (CAV '00), July, 2000.
• Binary Decision Diagrams and Symbolic Model Checking
  Invited talk, Symposium on Algorithms in the Real World, May, 2000.
• Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions
  Computer-Aided Verification (CAV '99), July, 1999.
• Optimizing Symbolic Model Checking for Constraint-Rich Systems
  Computer-Aided Verification (CAV '99), July, 1999.
• Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams
  August, 1999