Office Hours

In Spring, 2023, I will be teaching CS340d. If you would like to talk with me, please send me an E-mail message to schedule an appointment.

Course Information

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

    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 biological-inspired computing. Currently, I am working on rapid, single-flux quantum (RSFQ) computing, specifying computer memory models, and extending our ACL2-based x86 specification. Additional details are available.

    Accomplishments

  • My primary contributions concern the formal specification and verification of digital computing systems. I am currently involved with the study of RSFQ circuits and X86 ISA specification and design validation. I also worked briefly in the area of computational biology. I have listed some of these efforts.

    Papers, Resume, and Personal Information

  • In my vita is a listing of all of my papers; there are also links to each of my papers. Out of consideration for my references, I do not include their names and contact information on the Web, but they are available upon request. A short biography is also available.

    My Google Scholar page can be used to find most of my publications.

    Research Topics

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

    Some Talks

    In 2024, I gave a talk at the Newton Institute (in Cambridge, UK) about using the ACL2 x86-ISA model to boot Linux and to execute Linux programs.

    In 2021, J Moore and I gave a litany of lectures about the use of ACL2; look part way down this webpage for our names.

    This is a talk given at the Newton Institute about Centaur Technology's use of ACL2 to specify and verify properties of VIA x86 microprocessor designs.

    In 2017, I gave an invited talk to the JASON Advisory Group about our hardware-focused efforts.

    In 2016, I gave an invited talk at the Royal Society about our specifying the x86 ISA and our use of this specificaiton.

    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

    For nearly two decades, I served as chairman of the FMCAD steering committee; I stepped down in 2020. 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 & Amazon Scientist.

  • Jo Ebergen -- PhD & Retired Senior Consulting Engineer, Oracle.

  • Shilpi Goel -- PhD & Engineer, Intel Corporation.

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

  • J Strother Moore -- UTCS Professor Emeritus.

  • David Rager -- PhD & Finance Scientist.

  • Sandip Ray -- PhD & Endowed IoT Term Professor, University of Florida at Gainesville.

  • Marly Roncken -- Senior Research Associate, Portland State University.

  • Anna Slobodova -- PhD & Senior Principal Engineer, ARM Corporation.

  • Rob Sumners -- PhD & Principal Engineer, AMD Corporation.

  • Ivan Sutherland -- Research Professor, Portland State University.

  • Sol Swords -- PhD & Principal Engineer, ARM Corporation.

  • Mertcan Temel -- PhD & Engineer, Intel Corporation.

  • Nathan Weltzer -- PhD & Senior Engineer, Apple Corporation.

    Current PhD Students:

    PhD students that work in my research group.

  • Balasubraman Muthuvelu -- ECE PhD Student.

  • Gavin Meil -- CS PhD Student.

    Current PhD Candidates:

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

  • Carl Kwan -- CS PhD Candidate.

    Graduated PhDs

  • 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.

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

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

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

  • Nathan Weltzer -- CS PhD, co-advised with Marijn Heule, Spring, 2015.

  • Shilpi Goel -- CS PhD, Fall, 2016.

  • Cuong Chau -- CS PhD, Spring, 2019.

  • Mertcan Temel -- CS PhD, Summer, 2021.

    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.