Office Hours

For Fall, 2012, my office hours Mondays from 16:00 to 18:00 (althought I am often there later) in Painter Hall, 5th floor, outside of the computer laboratory. Certainly, other times are available; please send me an E-mail to schedule 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 specifying computer memory models. Addtional details are available.

Course Information

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

    Personal Information

  • My resume is available. Out of consideration for my references, I don't include their names and contact information on the Web, but they are available upon request.

    Research Topics

  • I am working on several research topics. Please contact me if you desire additional information.

    Some Talks

    I gave an invited talk at ITP 2011, about our work with Centaur Technology, Inc., where we are verifying various properties of the 64-bit, VIA Nano, X86-compatible microprocessor.

  • I gave a talk at CAV 2009 about my work with Sol Swords regarding our efforts at applying our tools to VIA's Nano processor.

  • I was one several presenters 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. The FMCAD conference series has existed since 1996. The conference is supported by FMCAD, Inc., and the conference has enjoyed "in-kind" support from the ACM and the IEEE. For 1996 -- 2004, FMCAD conference proceeding were published in Springer's LNCS. Since 2005, FMCAD conference papers are available in the ACM and IEEE digital libraries. Additional details about FMCAD are available.

    Professional Associates

  • Robert S. Boyer -- UTCS Professor Emeritus.

  • Jared Davis -- PhD & Engineer.

  • Marijn Heule -- PhD & UTCS Research Fellow.

  • Matt Kaufmann -- PhD & UTCS Senior Research Scientist.

  • J Strother Moore -- UTCS Professor.

  • Sandip Ray -- PhD & Intel Research Scientist.

  • Anna Slobodova -- PhD & Principal Engineer.

  • Sol Swords -- PhD & Engineer.

  • Tandy Warnow -- UTCS Professor.

    Current PhD Students:

    PhD students that work in my research group.

  • Shilpi Goel -- CS PhD Student.

  • Robert Krug -- CS PhD Student.

  • Nathan Weltzer -- CS PhD Student.

    Current PhD Candidates:

    PhD students that have successfully proposed and for which I am acting as their principal advisor.

    Graduated PhD Students

  • Jun Sawada -- CS PhD, 1999.

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

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

  • Serita Nelesen -- CS PhD, co-advised with Tandy Warnow, Fall, 2009.

  • David Rager -- CS PhD, Fall, 2012.

  • Sol Swords -- CS PhD, Fall, 2010.

  • Ian Wehrman -- CS PhD, co-advised with J Moore, Fall, 2012.

    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.