Alan J. Hu
Dept. of Computer Science
Univ. of British Columbia
2366 Main Mall
Vancouver, BC V6T 1Z4
email (rendered as an image to foil spambots):
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.
Note that UBC Computer Science does graduate admissions via
an admissions committee, so it's pointless to send me generic
I-want-to-be-your-student emails. If you have very specific
background and interest in formal verification, I'll try to
answer email questions. Otherwise, just apply, come to UBC, meet all
the profs, take the courses, and if everything works out,
we might end up doing research together. A great thing about our
department is that you have enormous freedom after you arrive to
choose your research area and advisor.
Formal Verification Courses
I'm teaching a course on formal verification of finite-state systems
(mainly hardware, but relevant to some software).
This links to the course home page (CPSC 513).
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!" :-)
``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).)
Papers, Theses, Tech Reports
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
Current Students (in order of expected graduation)
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!)
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
as test cases for our high-lvel-vs.-RTL verification
The software model has complicated control flow, but
is combinationally (single-cycle) equivalent to the
structurally different RTL.
our 2006 DAC paper for
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
SPUDD: Stochastic Planning Using Decision Diagrams
Robert St. Aubin
under the guidance
Craig Boutilier and myself, SPUDD is a powerful tool for
planning with Markovian decision processes.
SPUDD Home Page
has publications, the software, and even an interactive interface to
submit your problems to run on our SPUDD servers.
developed a parallelized BDD package based on
Fabio Somenzi's CUDD package
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
You will need to have
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!
- 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