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 PseudoBoolean Reasoning.
Presentation at TACAS 2022.
 Dual Proof Generation for Quantified Boolean Formulas with a BDDBased Solver.
Presentation at CADE 2021.
 Generating Extended Resolution Proofs with a BDDBased SAT Solver.
Presentation at TACAS 2021.
 Generating Extended Resolution Proofs with a BDDBased SAT Solver.
Presentation at TACAS 2021.
 Chain Reduction for Binary and ZeroSuppressed 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 mathematicallyoriented high school students.
Also available
in PDF format.

Computers+Robots
A brief presentation on artificial intelligence and robotics, intended for middle and highschool 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 ComputerAided Design
Austin, TX, November, 2007.
Modified version
at VLSI Design and Test, Taiwan, 2008.
 DataIntensive Super Computing. Two versions:

BitVector 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 InfiniteState 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
USChina Computer Science Leadership Summit, Beijing, May 23, 2006.

Formal Verification of InfiniteState 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:

Symbolic, WordLevel Hardware Verification
Embedded Tutorial,
International Conference on ComputerAided Design (ICCAD '04),
November, 2004.

System Modeling and Verification with UCLID
Keynote Presentation, MemoCODE 2004,
June, 2004.
 SATBased Decision Procedures for Subsets of FirstOrder Logic

Convergence Testing in TermLevel Bounded Model Checking
Correct Hardware Design and Verification Methods (Charme '03), November, 2003.

Formal Verification of InfiniteState Systems using Boolean Methods
Distinguished Lecture, University of Pennsylvania
Computer Science Department, October, 2003.

Deductive Verification of Advanced OutofOrder Microprocessors
ComputerAided Verification (CAV '03), July, 2003.

Unbounded, Fully Symbolic Model Checking of Timed Automata using Boolean Methods
ComputerAided Verification (CAV '03), July, 2003.

A Hybrid SATBased Decision Procedure for Separation Logic and Uninterpreted Functions
Design Automation Conference (DAC '03), June, 2003.

Formal Verification Using InfiniteState Models
Distinguished Lecture, UCLA Computer Science Department, March, 2003.

Symbolic Simulation and its Connection to Formal Verification
Invited talk, Formal Methods in ComputerAided Design, November, 2002.

Modeling and Verification of OutofOrder Processors in UCLID
Formal Methods in ComputerAided Design, November, 2002.

Modeling and Verifying Systems using a Logic of Counter Arithmetic
with Lambda Expressions and Uninterpreted Functions
ComputerAided Verification (CAV '02), July, 2002.

Deciding Separation Formulas with SAT
ComputerAided Verification (CAV '02), July, 2002.

Boolean Satisfiability with Transitivity Constraints
ComputerAided 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
ComputerAided Verification (CAV '99), July, 1999.

Optimizing Symbolic Model Checking for ConstraintRich Systems
ComputerAided Verification (CAV '99), July, 1999.

Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams
August, 1999
Back to Randy Bryant's home page