Randal E. Bryant, Selected Presentations

Some of these presentations are Microsoft Powerpoint files (extension pptx), while others are in Adobe Acrobat (extension pdf).

• Clausal Proofs for Pseudo-Boolean Reasoning. Presentation at TACAS 2022.
• Dual Proof Generation for Quantified Boolean Formulas with a BDD-Based Solver. Presentation at CADE 2021.
• Generating Extended Resolution Proofs with a BDD-Based SAT Solver. Presentation at TACAS 2021.
• Chain Reduction for Binary and Zero-Suppressed Decision Diagrams. Presentation at TACAS 2018.
• Creating a Foundational Curriculum in Computer Science. Keynote presentation at University Course Forum in Computer Science, Guanzhou, China, November, 2012.
• MapReduce Programming. Presented to students in "Introduction to Computer Systems" at Peking University, November, 2012.
• Solving Graph Problems with Boolean Methods. A presentation on how to encode different graph problems as Boolean formulas and then find solutions via either BDDs or SAT solvers. Targeted to mathematically-oriented high school students. Also available in PDF format.
• Computers+Robots A brief presentation on artificial intelligence and robotics, intended for middle and high-school students. Lots of videos, very few words. This is a "tgz" file of a directory containing powerpoint and video files.
• 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

---

Back to Randy Bryant's home page