Randal Bryant
Dean – SCS; Professor – CS, ECE
| Contact Information | |
|---|---|
| Department | School of Computer Science |
| Office | 4301 Newell-Simon Hall |
| Telephone | (412)-268-8821 |
| Fax | (412)-268-5577 |
| bryant@cs.cmu.edu | |
| Website | http://www.cs.cmu.edu/~bryant/ |
Research Interests
Professor Bryant's primary research interest is in formally verifying hardware designs. This interest grew out of earlier work in logic simulation and symbolic circuit analysis. Formal verification promises to eliminate the uncertainty that lingers even after extensive evaluation by techniques such as simulation.
During the course of developing hardware verification tools, he has become interested in symbolic representations and manipulation of discrete functions. The approach followed involves representing functions by directed acyclic graphs, known as Binary Decision Diagrams (BDDs). These methods are now being applied not just to circuit verification, but also to such areas as: temporal logic model checking, logic circuit optimization, automated theorem proving and truth maintenance systems.
Most recently, he has focused on the verification of superscalar microprocessors. In an effort to maximize the speed of program execution, modern processors apply techniques such as out-of-order execution, speculation and many forms of caching. Verifying that such a system faithfully preserves the sequential execution model of the instruction set architecture is both an intellectual and a logistical challenge. Recently developed techniques allow much of the data processing operations to be abstracted away, allowing the verifier to concentrate on control and communication. By exploiting properties of these abstract models, increasingly complex processors can be formally verified.
In the News
- ECE Faculty Win Awards at DAC
- ECE Alumnus Wins Outstanding Dissertation Award from ACM SIGDA
- Bryant Named New School of Computer Science Dean
- Bryant's National Academy of Engineering Reception Held
- Bryant Elected to National Academy of Engineering
- Zamora Awarded SRC Graduate Fellowship
- CMU Faculty Awarded More Than $24 Million in Grants From NSF's ITR Initiative
- Bryant's Paper Most Cited on Scientific Digital Library
Keywords
Formal hardware and software verification
Education
PhD, 1981
Electrical Engineering and Computer Science
MIT
EE, 1978
Electrical Engineering
MIT
SM, 1977
Electrical Engineering
MIT
BS, 1973
Applied Mathematics
University of Michigan, Ann Arbor