Alan J. Hu Dept. of Computer Science Univ. of British Columbia 2366 Main Mall Vancouver, BC V6T 1Z4 Canada tel: +1-604-822-6667 fax: +1-604-822-5485 email (rendered as an image to foil spambots):

Email Warning: I'm often in a state of email bankruptcy. If you need a timely reply and haven't heard from me, please stop by or try calling. Physical mail is also generally reliable.

Welcome to my quick-and-dirty home page. This page exists simply to make it easier for people to get documents and software from me. I'll make a really spiffy home page to show off what a net-savvy Generation X slacker I am when I have nothing better to do.

Prospective Graduate Students

UBC is a great place to do your masters or PhD! Admission is extremely competitive, but if you're up for the challenge, please consider applying. See our graduate admissions welcome page for more information.

Formal Verification Courses

I previously taught another course on this topic in Spring 1996-1997. This links to the old home page for CPSC 538D.

For people looking for a quick introduction, here is a short, introductory paper on hardware verification with BDDs. It appeared in PACRIM in 1997, (Please see my publication list for full bibliographic information.) so it is a bit dated and limited, but it still makes a nice introduction. I wrote it with the goal of creating the simplest presentation of this material that still has technical content. I've often received compliments about this paper along the lines of, "It was so simple, I could even give it to my manager!" :-)

Talks

• ``The Amazing Commercial Success of Formal Verification,'' I gave this talk at the Xerox PARC Forum on November 11, 1999. A number of people have asked me for copies of the slides, so here are the slides in gzipped postscript (43k) as well as a plaintext abstract. The slides are extremely sketchy but the talk was videotaped. (I believe PARC employees have access to the videotape.) I also signed a release for MURL, and the video is apparently available from them in Windows Media Player format. I don't normally use Windows machines, so I haven't checked the audio/video quality. (Update 2011-8-15: Sadly, MURL apparently got folded into ResearchChannel, which eventually shut down due to lack of funds. I can no longer find any copy of this video, and never made a copy. If anyone knows how to get a hold of old MURL videos, I'd love to get a copy of this talk (and many others).)

Students

I've been lucky to work with some really amazing students over the years. I'm often asked by people with job openings whether I have any students graduating soon, and I'm always flattered to be asked (since it's really the students' credit). To help anyone tracking the pipeline, I'm listing my students here:

Current Students (in order of expected graduation)

• Malte Schwerin
• Stuart Hoad

Former Students (reverse chronological order)

(BTW, if you're my former student and want a link to your webpage here (or need it updated), please let me know!)

• Nodir Kodirov
• Syed Iqbal
• May Young
• Itrat Akhter
• Sam Bayless
• Andrew "Kuba" Karpierz
• Mike Enescu
• Ricardo Ochoa
• Celina Val
• Kyle Balston
• Mehdi Karimibiuki
• Flavio M. de Paula
• Zvonimir Rakamaric
• Domagoj Babic
• Xiushan "Shaun" Feng
• Jesse Bingham
• Kelvin Ng
• Marcio T. Oliveira
• Felix Sheng-Ho Chang
• Brian D. Winters
• David W. Currie

Software, Benchmarks, Data Sets, etc.

• MonoSAT, a SAT Modulo Theories (SMT) solver for Boolean monotonic theories. This provides an efficient solver for reasoning about a wide set of graph properties, some geometric properties, and some other theories, all in an SMT context.
• SAT Modulo SAT. ModSAT is a SAT solver structured as an SMT solver, in which SAT solvers for individual modules of a design behave as theory solvers (for the "theory" of that module) in a Lazy SMT framework. The solver also builds Craig interpolates "for free", without any proof extraction or processing. Based on this, we have created a very high performance version of IC3.
• Intel IA-32 Subset Instruction Length Decoder Examples. This is a suite of C software models and functionally equivalent RTL Verilog models, developed by Xiushan Feng as test cases for our high-lvel-vs.-RTL verification research. The software model has complicated control flow, but is combinationally (single-cycle) equivalent to the structurally different RTL. Please see our 2006 DAC paper for details.
• PREMiS Version 0.1 is a Pipelined Regular Expression Monitor Specification system developed by Marcio Oliveira for his master's thesis. This is a proof-of-concept language for the idea of providing built-in support for specifying pipelined interfaces in a very natural style, and then having the tool automatically generate a monitor circuit for the interface. See Marcio's thesis or our 2002 DAC paper for details.
• SPUDD: Stochastic Planning Using Decision Diagrams Developed by Jesse Hoey and Robert St. Aubin under the guidance of Craig Boutilier and myself, SPUDD is a powerful tool for planning with Markovian decision processes. The SPUDD Home Page has publications, the software, and even an interactive interface to submit your problems to run on our SPUDD servers.
• Kim Milvang-Jensen developed a parallelized BDD package based on Fabio Somenzi's CUDD package Version 2.1.2, while working with me at UBC. I believe we were the first to report speed-up on a network of workstations over non-thrashing, optimized sequential code. You can download a copy of Kim's thesis as well as the BDDNOW package. You will need to have PVM installed on your machine to use BDDNOW.
• The Ever verifier was originally intended as a BDD-based back-end for the Murphi system, but has since mutated into a research workbench for testing out techniques for effectively using BDDs on practical-sized, high-level verification problems. Ever Version 0.1 is finally available for downloading. It's ugly! It's poorly documented! But it exists! You may want to read the README file first, which contains my "license" terms.
• The Murphi verification system is an easy-to-use, finite-state automatic verifier. We've found it useful on several real-life examples, including cache coherence protocols, multiprocessor memory models, link-level protocols and highly-pipelined processors. Several people from industry tell us that they, too, found it very useful, especially considering the price they paid. Get more information and your very own free copy of the latest version from sprout.stanford.edu.

Recent Research Support Acknowledgments

I've been fortunate to have strong support for my research, from both industry and government funding sources. Some sources request that their funding be acknowledged; others don't. I am listing some recent research support here. (If you funded me and don't want me to list you, or if you want to be linked, or a logo displayed, please let me know!) A big THANK YOU to these folks who help make my research possible!

• IBM
• Intel Corporation
• Lockheed-Martin Corporation
• Microsoft Research
• Natural Sciences and Engineering Research Council of Canada (NSERC)
• Semiconductor Research Corporation (SRC)

Copyright 1998-2007 Alan J. Hu

Last Modified: 2013 August 31