Office Hours

For Spring, 2008, my office hours are on Wednesdays, from 5:45 until 6:45 pm. Other times are possible -- send me E-mail to make an appointment.

Interest Areas

My research involves the use of formal mathematics to write specifications for computer hardware and software and to use proof techniques to determine the validity of such specifications. Specifications of both high-level intent and low-level implementations are possible, and mechanical proof techniques can determine whether implementations satisfy their specifications. Over the years, I have verified a number of different microprocessor designs of increasing complexity.

I am also interested in computer architecture, low-power computing, garbage collection, and parallel computing. Currently, I am working on a Hash CONS implementation, to parallelize several theorem-proving algorithms, and I am working on computational biology consensus algorithms. Addtional details are available.

Course Information

  • Notes and information for my courses are on-line. I would appreciate any feedback and corrections.

    Some Talks

  • I was one of three presenters (Randy Bryant and Robert Jones) at the CAV2004 tutorial on microprocessor verification. I presented slides outlining the difficulty of identifying microprocessor correctness statements, and I presented a summary of the verification of the FM9801 (Jun Sawada's PhD Dissertation work) as an example microprocessor verification effort. In the second part of my presentation, I presented slides with some thoughts of what facilities future hardware verifications system should include.

    FMCAD

    I am chairman of the FMCAD steering committee. Details about FMCAD are available.

    PhD Students

    Current:

  • Serita Nelesen -- CS PhD Candidate

  • David Rager -- CS PhD Student

  • Sol Swords -- CS PhD Student

    Past:

  • Jun Sawada -- CS PhD

  • Shant Harutunian -- ECE PhD, Spring, 2007.

  • Erik Reeber -- CS PhD, Fall, 2007.

    Standard disclaimer

    Nothing on my web pages should be taken as representing the official position of the University of Texas at Austin or any other part of the government of the State of Texas.

    Up

    To the University of Texas at Austin Computer Sciences Department.