Published Papers and Other Documents

Published Papers: recent, 2008, 2007, 2006, 2005, 2000-2004, 1995-1999, before 1995.
Theses
Tech Reports and Other Documents
Alan J. Hu's Home Page

Published Papers

Recent

  • Zvonimir Rakamaric, and Alan J. Hu, ``A Scalable Memory Model for Low-Level Code,'' Verification, Model Checking, and Abstract Interpretation: 10th International Conference (VMCAI), Lecture Notes in Computer Science Vol. 5403, pp. 290-304, Springer, 2008. (The conference was in January 2009.) This paper is Copyright 2008 by Springer. The original publication is available at www.springerlink.com. (That wording is required in the Springer copyright transfer form when this was written. Basically, the definitive on-line publication is using that link.) (BibTeX Entry)

    • 2008

  • Flavio M. De Paula, Marcel Gort, Alan J. Hu, and Steven J. E. Wilton, ``BackSpace: Moving Towards Reality,'' Ninth International Workshop on Microprocessor Test and Verification, IEEE Computer Society, 2008, pp. 49-54. This paper is Copyright 2009 by the IEEE. Link to the definitive version of the paper at IEEE Xplore.

  • Flavio M. De Paula, Marcel Gort, Alan J. Hu, Steven J. E. Wilton, and Jin Yang, ``BackSpace: Formal Analysis for Post-Silicon Debug,'' Formal Methods in Computer-Aided Design (FMCAD), IEEE eXpress Publishing, 2008, pp. 35-44. This paper is Copyright 2008 by the IEEE. Link to the definitive version of the paper at IEEE Xplore.

  • Zvonimir Rakamaric, and Alan J. Hu, ``Automatic Inference of Frame Axioms Using Static Analysis,'' 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE), IEEE eXpress Publishing, 2008, pp. 89-98. This paper is Copyright 2008 by the IEEE. Link to the definitive version of the paper at IEEE Xplore. (BibTeX Entry)

  • Domagoj Babic, and Alan J. Hu, ``Calysto: Scalable and Precise Extended Static Checking,'' 30th International Conference on Software Engineering (ICSE), ACM, 2008, pp. 211-220. This work is Copyright ACM, 2008. The definitive version of the paper was published as stated above, and is available on-line at http://doi.acm.org/10.1145/1368088.1368118 . (BibTeX Entry)

    • 2007

  • Frank Hutter, Domagoj Babic, Holger H. Hoos, and Alan J. Hu, ``Boosting Verification by Automatic Tuning of Decision Procedures,'' Formal Methods in Computer-Aided Design (FMCAD), IEEE eXpress Publishing 2007, pp. 27-34. This paper is Copyright 2007 by the IEEE. Link to the definitive version of the paper at IEEE Xplore. In addition, I am providing links to my personal copy, for your personal use, not for sale, and with no implied endorsement by the IEEE (in accordance with IEEE's Copyright Policy). (PDF) (BibTeX Entry) (Plain Text Abstract)

  • Domagoj Babic, and Alan J. Hu, ``Exploiting Shared Structure in Software Verification Conditions,'' Third International Haifa Verification Conference, HVC 2007, Lecture Notes in Computer Science Vol. 4899, pp. 169-184, Springer, 2008.

  • Zvonimir Rakamaric, Roberto Bruttomesso, Alan J. Hu, and Alessandro Cimatti, ``Verifying Heap-Manipulating Programs in an SMT Framework,'' Automated Technology for Verification and Analysis: 5th International Symposium (ATVA), Lecture Notes in Computer Science Vol. 4762, pp. 237-252, Springer, 2007. This paper is Copyright 2007 by Springer. The original publication (i.e., the definitive on-line version) should appear at www.springerlink.com soon. With Springer's permission, I am providing links to my personal copy, on my personal archive. (PDF) (BibTeX Entry) (Plain Text Abstract)

  • Domagoj Babic, Alan J. Hu, Zvonimir Rakamaric, and Byron Cook, ``Proving Termination by Divergence,'' 5th IEEE International Conference on Software Engineering and Formal Methods (SEFM), IEEE Computer Society Press, 2007, pp. 93-102. This paper is Copyright 2007 by the IEEE. Link to the definitive version of the paper at IEEE Xplore.

  • Domagoj Babic, and Alan J. Hu, ``Structural Abstraction of Software Verification Conditions,'' Computer Aided Verification: 19th International Conference (CAV), Lecture Notes in Computer Science Vol. 4590, pp. 366-378, Springer, 2007. This paper is Copyright 2007 by Springer. The original publication (i.e., the definitive on-line version) should appear at www.springerlink.com soon. With Springer's permission, I am providing links to my personal copy, on my personal archive. (PDF) (BibTeX Entry) (Plain Text Abstract)

  • Flavio M. de Paula, and Alan J. Hu, ``An Effective Guidance Strategy for Abstraction-Guided Simulation,'' 44th ACM/IEEE Design Automation Conference (DAC), pp. 63-68, 2007. This work is Copyright ACM, 2007, and is available on-line via IEEE Xplore . If the definitive link is dead for some reason, here are links to my own, personal version of the work, posted by permission of ACM for your personal use, and not for redistribution. (PDF) (BibTeX Entry) (Plain Text Abstract)

  • Zvonimir Rakamaric, Jesse Bingham, and Alan J. Hu, ``An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures,'' Verification, Model Checking, and Abstract Interpretation: 8th International Conference (VMCAI), Lecture Notes in Computer Science Vol. 4349, pp. 106-121, Springer, 2007. This paper is Copyright 2007 by Springer. The original publication (i.e., the definitive on-line version) should appear at www.springerlink.com soon. With Springer's permission, I am providing links to my personal copy, on my personal archive. (PDF) (BibTeX Entry) (Plain Text Abstract)

    • 2006

  • Domagoj Babic, Jesse Bingham, and Alan J. Hu, ``B-Cubing: New Possibilities for Efficient SAT-Solving,'' IEEE Transactions on Computers, Vol. 55, No. 11 (November 2006), pp. 1315-1324. Link to the definitive on-line version of the paper through IEEE Xplore.

  • Alan J. Hu, ``High-Level vs. RTL Combinational Equivalence: An Introduction,'' IEEE International Conference on Computer Design (ICCD), pp. 274-279, 2006. This paper is Copyright 2006 by the IEEE. A link to the definitive version of the paper will appear here when I find that it is available at IEEE Xplore. In the interim, here is a link to the final version from the ICCD website. In addition, I am providing links to my personal copy, for your personal use, not for sale, and with no implied endorsement by the IEEE (in accordance with IEEE's Copyright Policy). (PDF) (BibTeX Entry) (Plain Text Abstract)

  • Flavio M. de Paula, and Alan J. Hu, ``EverLost: A Flexible Platform for Industrial-Strength Abstraction-Guided Simulation,'' Computer Aided Verification: 18th International Conference (CAV), Lecture Notes in Computer Science Vol. 4144, pp. 282-285, Springer, 2006. This paper is Copyright 2006 by Springer. The original publication is available at www.springerlink.com. (That wording is required in the Springer copyright transfer form when this was written. Basically, the definitive on-line publication is using that link.) With Springer's permission, I am providing links to my personal copy, on my personal archive. (PDF) (BibTeX Entry) (Plain Text Abstract)

  • Xiushan Feng, and Alan J. Hu, ``Early Cutpoint Insertion for High-Level Software vs. RTL Formal Combinational Equivalence Verification,'' 43rd ACM/IEEE Design Automation Conference (DAC), 2006, pp. 1063-1068. This work is Copyright ACM, 2006. The definitive version of the paper was published as stated above, and is available on-line at http://doi.acm.org/10.1145/1146909.1147178 . If the definitive link is dead for some reason, here are links to my own, personal version of the work, posted by permission of ACM for your personal use, and not for redistribution. (PDF) (BibTeX Entry) (Plain Text Abstract)

  • Resve Saleh, Steve Wilton, Shahriar Mirabbasi, Alan Hu, Mark Greenstreet, Guy Lemieux, Partha Partim Pande, Cristian Grecu, and Andre Ivanov, ``System-on-Chip: Reuse and Integration,'' Proceedings of the IEEE, Vol. 94, No. 6 (June 2006), pp. 1050-1069. Link to the definitive on-line version of the paper through IEEE Xplore.

  • David Currie, Xiushan Feng, Masahiro Fujita, Alan J. Hu, Mark Kwan, and Sreeranga Rajan, ``Embedded Software Verification Using Symbolic Execution and Uninterpreted Functions,'' International Journal of Parallel Programming, Vol.~34, No.~1 (March 2006), pp.~61--91. Link to the definitive on-line version of the paper through SpringerLink.

    • 2005

  • Domagoj Babic, Jesse D. Bingham, and Alan J. Hu, ``B-Cubing Theory: New Possibilities for Efficient SAT-Solving,'' 10th IEEE International High-Level Design Validation and Test Workshop (HLDVT), 2005, pp. 192-199. This paper is Copyright 2005 by the IEEE. A link to the definitive version of the paper will appear here when it becomes available at IEEE Xplore. In the interim, I am providing a link to my personal copy: (PDF) (Gzipped Postscript) (BibTeX Entry) (Plain Text Abstract)

  • Xiushan Feng, and Alan J. Hu, ``Cutpoints for Formal Equivalence Verification of Embedded Software,'' 5th ACM International Conference on Embedded Software (EMSOFT), 2005, pp. 307-316. This paper is Copyright 2005 by ACM Inc. Link to the definitive version of the paper at the ACM Digital Library. If the definitive link is dead for some reason, here is an unofficial copy, posted by permission of ACM for your personal use and not for redistribution: (Gzipped Postscript) (PDF) (BibTeX Entry) (Plain Text Abstract)

  • Domagoj Babic, Jesse D. Bingham, and Alan J. Hu, ``Efficient SAT Solving: Beyond Supercubes,'' 42nd ACM/IEEE Design Automation Conference (DAC), 2005, pp. 744-749. This paper is Copyright 2005 by ACM Inc. Link to the definitive version of the paper at the ACM Digital Library. If the definitive link is dead for some reason, here is an unofficial copy, posted by permission of ACM for your personal use and not for redistribution: (PDF) (BibTeX Entry) (Plain Text Abstract)

  • Jesse Bingham, and Alan J. Hu, ``Empirically Efficient Verification for a Class of Infinite-State Systems,'' Tools and Algorithms for the Construction and Analysis of Systems: 11th International Conference (TACAS), Lecture Notes in Computer Science Vol. 3440, pp. 77-92, Springer, 2005. This paper is Copyright 2005 Springer. The definitive on-line version of this paper is available on-line through Springer's SpringerLink on-line access. I am providing here a link to an extended version of the paper, which fixes some typos and adds proofs to the published conference version. This extended version is also available as UBC Computer Science technical report TR 2005-07. (See Technical Reports below.) (PDF) (Gzipped Postscript) (BibTeX Entry) (Plain Text Abstract)

  • Michael R. Marty, Jesse D. Bingham, Mark D. Hill, Alan J. Hu, Milo M. K. Martin, David A. Wood, ``Improving Multiple-CMP Systems Using Token Coherence,'' IEEE 11th International Symposium on High-Performance Computer Architecture (HPCA), IEEE Press, 2005, pp. 328-339. This paper is Copyright 2005 by the IEEE. The PDF linked here contains an additional, 1-page appendix of supporting data not included in the published version of the paper. (PDF) (BibTeX Entry) (Plain Text Abstract)

  • Xiushan Feng, Alan J. Hu, and Jin Yang, ``Partitioned Model Checking from Software Specifications,'' Asia South Pacific Design Automation Conference (ASPDAC), IEEE Press, 2005, pp. 583-587. This paper is Copyright 2005 by the IEEE. (Gzipped Postscript) (BibTeX Entry) (Plain Text Abstract)

  • Domagoj Babic, and Alan J. Hu, ``Integration of Supercubing and Learning in a SAT Solver,'' Asia South Pacific Design Automation Conference (ASPDAC), IEEE Press, 2005, pp. 438-444. This paper is Copyright 2005 by the IEEE. (PDF) (BibTeX Entry) (Plain Text Abstract)

    • 2004

  • Kelvin Ng, Alan J. Hu, and Jin Yang, ``Generating Monitor Circuits for Simulation-Friendly GSTE Assertion Graphs,'' IEEE International Conference on Computer Design (ICCD), IEEE Computer Society Press, 2004, pp. 488-492. This paper is Copyright 2004 by the IEEE. The following links are unofficial, personal-use copies provided for scholarly convenience, as is customary in academia. (Gzipped Postscript) (BibTeX Entry) (Plain Text Abstract)

  • Drew Dean, and Alan J. Hu, ``Fixing Races for Fun and Profit: How to use access(2),'' 13th USENIX Security Symposium, 2004, pp. 195-206. This paper is Copyright 2004 by the USENIX Association. The official on-line versions of this paper are now freely available from USENIX, with their permission. These are unofficial versions, posted here by permission of USENIX: (PDF) (BibTeX Entry) (Plain Text Abstract) NOTE: The scheme proposed here has been beautifully and thoroughly demolished by Nikita Borisov, Rob Johnson, Naveen Sastry, and David Wagner. The theory is, of course, still valid, but it relies on an assumption of the attacker having a non-negligible probability of losing races. Borisov et al. came up with ingenious means (1) to force the victim to go to disk on each race, thereby allowing plenty of time for the attacker to win races, and (2) to determine precisely what protocol operation the victim is doing at any point in time, thereby foiling the randomized delays. The upshot is that they can win these TOCTTOU races with almost complete certainty. Please see their 2005 USENIX Security Symposium paper for details. NOTE^2: Wow, this is very cool: Dan Tsafrir figured out a really clever way to restructure the races, such that it defeats the Borisov et al. filesystem maze attack. Dan Tsafrir, Tomer Hertz, David Wagner, and Dilma Da Silva have subsequently generalized the argument. The Borisov et al. filesystem mazes are a general technique to make filesystem TOCTTOU races easy to exploit, and the Tsafrir et al. hardness amplification is a general approach to defeat such attacks, resurrecting the original idea. In a nutshell, the key weakness in the original approach was our reliance on system calls that could be slowed down: they were not constant-time, and the attacker was able to slow them down by extreme amounts. The solution is to simulate the effect of these system calls using only constant-time calls, and then do the hardness amplification at this finer level of granularity. They have a USENIX FAST 2008 paper and a subsequent ACM Transactions on Storage paper , which are probably the definitive word on this topic.

  • Jesse Bingham, Anne Condon, Alan J. Hu, Shaz Qadeer, and Zhichuan Zhang, ``Automatic Verification of Sequential Consistency for Unbounded Addresses and Data Values,'' Computer Aided Verification: Sixteenth International Conference (CAV), Lecture Notes in Computer Science Vol. 3114, pp. 427-439, Springer, 2004. This paper is Copyright 2004 Springer-Verlag. The definitive on-line version of this paper is available on-line through Springer's LINK on-line access to Lecture Notes in Computer Science. If there are problems with access, I am providing a link to my personal copy: (PDF) (Gzipped Postscript) (BibTeX Entry) (Plain Text Abstract)

    • 2003

  • Alan J. Hu, Jeremy Casas, and Jin Yang, ``Efficient Generation of Monitor Circuits for GSTE Assertion Graphs,'' IEEE/ACM International Conference on Computer-Aided Design (ICCAD), 2003, pp. 154-159. This paper is Copyright 2003 by ACM Inc. Link to the definitive version of the paper at the IEEE Computer Society Digital Library. If the definitive link is dead for some reason, here is an unofficial copy: (Gzipped Postscript) (PDF) (BibTeX Entry) (Plain Text Abstract)

  • Alan J. Hu, Jeremy Casas, and Jin Yang, ``Reasoning about GSTE Assertion Graphs,'' 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME), Lecture Notes in Computer Science Vol. 2860, pp. 170-184, Springer, 2003. This paper is Copyright 2003 Springer-Verlag. The definitive on-line version of this paper is available on-line through Springer's LINK on-line access to Lecture Notes in Computer Science. If there are problems with access, I am providing a link to my personal copy: (Gzipped Postscript) (BibTeX Entry) (Plain Text Abstract)

  • Anne E. Condon and Alan J. Hu, ``Automatable Verification of Sequential Consistency,'' Theory of Computing Systems, Volume 36, Number 5, September 2003, Springer-Verlag, pp. 431-460. This is the extended journal version of our SPAA 2001 paper. This paper is Copyright 2003 Springer-Verlag. The definitive on-line version of this paper is available through Springer's LINK service.

  • Jesse D. Bingham, Anne E. Condon, and Alan J. Hu, ``Towards a Decidable Notion of Sequential Consistency,'' 15th ACM Symposium on Parallelism in Algorithms and Architectures (SPAA), pp. 304-313, ACM Press, 2003. This paper is Copyright 2003 by ACM Inc. Link to the definitive version of the paper at the ACM Digital Library. If the definitive link is dead for some reason, here is an unofficial copy: (Gzipped Postscript) (BibTeX Entry) (Plain Text Abstract)

    • 2002

  • Jesse D. Bingham, and Alan J. Hu, ``Semi-Formal Bounded Model Checking,'' Computer Aided Verification: Fourteenth International Conference (CAV), Lecture Notes in Computer Science Vol. 2404, pp. 280-294, Springer, 2002. This paper is Copyright 2002 Springer-Verlag. The definitive on-line version of this paper is available on-line through Springer's LINK on-line access to Lecture Notes in Computer Science. If there are problems with access, I am providing a link to my personal copy: (Gzipped Postscript) (PDF)

  • Xiushan Feng, and Alan J. Hu, ``Automatic Formal Verification for Scheduled VLIW Code,'' ACM SIGPLAN Joint Conference: Languages, Compilers, and Tools for Embedded Systems, and Software and Compilers for Embedded Systems (LCTES/SCOPES), pp. 85-92, ACM Press, 2002. This paper is Copyright 2002 by ACM Inc. Link to the definitive version of the paper at the ACM Digital Library. If the definitive link is dead for some reason, here is an unofficial copy: (Gzipped Postscript) ERRATUM

  • Marcio T. Oliveira, and Alan J. Hu, ``High-Level Specification and Automatic Generation of IP Interface Monitors,'' 39th ACM/IEEE Design Automation Conference (DAC), pp. 129-134, IEEE Press, 2002. This paper is Copyright 2002 by ACM Inc. Link to the definitive version of the paper at the ACM Digital Library. If the definitive link is dead for some reason, here is an unofficial copy: (Gzipped Postscript) (PDF)

    • 2001

  • Tim Braun, Anne Condon, Alan J. Hu, Kai S. Juse, Marius Laza, Michael Leslie, and Rita Sharma, ``Proving Sequential Consistency by Model Checking,'' IEEE International High-Level Design, Validation, and Test Workshop (HLDVT), pp. 103-108, 2001. (Gzipped Postscript)

  • Felix Sheng-Ho Chang and Alan J. Hu, ``Fast Specification of Cycle-Accurate Processor Models,'' IEEE International Conference on Computer Design (ICCD), pp. 488-492, 2001. (Gzipped Postscript)

  • Alvin R. Albrecht and Alan J. Hu, ``Register Transformations with Multiple Clock Domains,'' 11th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME), 2001, published in Springer Lecture Notes in Computer Science Vol. 2144, pp. 126-139, 2001. (Gzipped Postscript)

  • Anne E. Condon and Alan J. Hu, ``Automatable Verification of Sequential Consistency,'' 13th ACM Symposium on Parallel Algorithms and Architectures (SPAA), pp. 113-121, 2001. (Gzipped Postscript) (PDF)

    • 2000

  • Kanna Shimizu, David L. Dill, and Alan J. Hu, ``Monitor-Based Formal Specification of PCI,'' Formal Methods in Computer-Aided Design (FMCAD), 2000, published in Springer Lecture Notes in Computer Science Vol. 1954, pp. 335-353, 2000. (Gzipped PDF)

  • Brian D. Winters and Alan J. Hu, ``Source-Level Transformations for Improved Formal Verification,'' IEEE International Conference on Computer Design (ICCD), pp. 599-602, 2000. (Gzipped Postscript)

  • David W. Currie, Alan J. Hu, Sreeranga Rajan, and Masahiro Fujita, ``Automatic Formal Verification of DSP Software,'' 37th ACM/IEEE Design Automation Conference (DAC), pp. 130-135, 2000. (Gzipped Postscript)

    • 1995-1999

  • Alan J. Hu, Rui Li, Xizheng Shi, and Son Vuong, ``Model-Checking a Secure Group Communication Protocol: A Case Study,'' IFIP TC6/WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing and Verification (FORTE/PSTV)}, 1999. (Gzipped Postscript)

  • Jesse Hoey, Robert St. Aubin, Alan J. Hu, and Craig Boutilier, ``SPUDD: Stochastic Planning using Decision Diagrams,'' 15th Conference on Uncertainty in Artificial Intelligence (UAI), pp. 279--288, 1999. (Gzipped Postscript) (PDF)

  • Kim Milvang-Jensen and Alan J. Hu, ``BDDNOW: A Parallel BDD Package,'' Formal Methods in Computer-Aided Design (FMCAD), 1998, published in Springer Lecture Notes in Computer Science Vol.~1522, pp.~501--507, 1998. (Gzipped Postscript)

  • Shankar G. Govindaraju, David L. Dill, Alan J. Hu, and Mark A. Horowitz, ``Approximate Reachability with BDDs Using Overlapping Projections,'' 35th ACM/IEEE Design Automation Conference (DAC), pp. 451-456, 1998. (Gzipped Postscript)

  • Alan J. Hu, Masahiro Fujita, and Chris Wilson, ``Formal Verification of the HAL S1 System Cache Coherence Protocol,'' IEEE International Conference on Computer Design (ICCD), pp.~438--444, 1997. (Gzipped Postscript)

  • ``Formal Hardware Verification with BDDs: An Introduction,'' IEEE Pacific Rim Conference on Communications, Computers, and Signal Processing (PACRIM), pp. 677-682, 1997. This is a short (6 pages) introductory article explaining the basics of the main BDD-based formal hardware verification techniques. (Gzipped Postscript)

    • Before 1995

  • Alan J. Hu, David L. Dill, and Gary York, ``New Techniques for Efficient Verification with Implicitly Conjoined BDDs,'' 31st ACM/IEEE Design Automation Conference (DAC), 1994, pp. 276--282. (Gzipped Postscript)

  • Alan J. Hu and David L. Dill, ``Efficient Verification with BDDs using Implicitly Conjoined Invariants,'' Computer Aided Verification: Fifth International Conference (CAV), 1993, published in Lecture Notes in Computer Science Vol. 697, Springer-Verlag, 1993. (Gzipped Postscript)

  • Alan J. Hu and David L. Dill, ``Reducing BDD Size by Exploiting Functional Dependencies,'' 30th ACM/IEEE Design Automation Conference (DAC), 1993, pp. 266--271. (Gzipped Postscript)

  • David L. Dill, Andreas J. Drexler, Alan J. Hu, and C. Han Yang, ``Protocol Verification as a Hardware Design Aid,'' IEEE International Conference on Computer Design (ICCD), 1992. (Gzipped Postscript)

  • Alan J. Hu, David L. Dill, Andreas J. Drexler, and C. Han Yang, ``Higher-Level Specification and Verification with BDDs,'' Computer Aided Verification: Fourth International Workshop (CAV), 1992, reprinted in Lecture Notes in Computer Science Vol. 663, Springer-Verlag, published 1993. (Gzipped Postscript)

  • Alan J. Hu and Gernot M. Engel, ``Minimizing Transmission Time in an SS/TDMA System with Variable Power Carriers,'' AIAA 14th International Communication Satellite Systems Conference, 1992.

  • David L. Dill, Alan J. Hu, and Howard Wong-Toi, ``Checking for Language Inclusion Using Simulation Relations,'' Computer Aided Verification: Third International Workshop (CAV), 1991, reprinted in Lecture Notes in Computer Science Vol. 575, Springer-Verlag, published 1992. (Definitive Version on Springer Link) (Personal Copy PDF) (Old Personal Copy Gzipped Postscript)

  • Alan J. Hu, ``Selection of the Optimum Uniform Partition Search,'' Computing, Vol. 37, No. 3 (1986), pp. 261-264.

    • Theses

  • My PhD Thesis, entitled ``Techniques for Efficient Formal Verification Using Binary Decision Diagrams,'' is available in gzipped postscript (260K), and also as Stanford University Department of Computer Science Technical Report Number CS-TR-95-1561 from the Stanford Electronic Library, which is a great place to find all sorts of technical reports and notes in general. (You can also anonymous ftp to elib.stanford.edu if you find yourself without a web browser.) The thesis is also available from my former research group at Stanford: [Abs] [Bib] [PS] Alan John Hu. "Efficient Techniques for Formal Verification Using Binary Decision Diagrams," Ph.D. Thesis, Stanford University, December 1995.

    • Below are theses done under my "supervision". This list is usually incomplete, as I'm lazy in tracking down my students' theses. If you want a thesis that isn't listed here, let me know, and I'll try to find it.

  • Kim Milvang-Jensen, ``BDDNOW: A Parallel BDD Package,'' M.Sc. Thesis, Department of Computer Science, University of Copenhagen, (DIKU), August 1998. (Gzipped Postscript) Kim did this work while visiting UBC for a year.

  • David W. Currie, ``A Tool for Formal Verification of DSP Assembly Language Programs,'' M.Sc. Thesis, University of British Columbia, August 1999. (Gzipped Postscript)

  • Brian D. Winters, ``Source-Level Transformations for Improved Formal Verification,'' M.Sc. Thesis, University of British Columbia, August 2000. (Copyright Info) (Abstract) (PDF) (Gzipped Postscript) (BibTeX)

  • Felix Sheng-Ho Chang, ``High-Level Cycle-Accurate Specification of Microprocessors,'' M.Sc. Thesis, University of British Columbia, August 2001. (Gzipped Postscript)

  • Xiushan Feng, ``Automatic Formal Verification for Scheduled VLIW Code,'' M.Sc. Thesis, University of British Columbia, August 2002.

  • Marcio T. Oliveira, ``High-Level Specification and Automatic Generation of IP Interface Monitors,'' M.Sc. Thesis, University of British Columbia, August 2003. (PDF)

    • Tech Reports and Other Documents

    All UBC Computer Science technical reports are available from http://www.cs.ubc.ca/cgi-bin/tr . I am providing the links below as shortcuts.

  • Zvonimir Rakamaric, Jesse Bingham, and Alan J. Hu, ``A Better Logic and Decision Procedure for Predicate Abstraction of Heap-Manipulating Programs,'' University of British Columbia Department of Computer Science Technical Report UBC CS TR-2006-02, January 30, 2006.

  • Jesse Bingham, and Alan J. Hu, ``Empirically Efficient Verification for a Class of Infinite-State Systems,'' University of British Columbia Department of Computer Science Technical Report UBC CS 2005-07, March 23, 2005.

  • Tim Braun, Anne Condon, Alan J. Hu, Kai S. Juse, Marius Laza, Michael Leslie, and Rita Sharma, ``Proving Sequential Consistency by Model Checking,'' University of British Columbia Department of Computer Science Technical Report UBC CS 2001-03, May 17, 2001.

  • Jesse Hoey, Robert St.Aubin, Alan Hu, and Craig Boutilier, ``Optimal and Approximate Stochastic Planning using Decision Diagrams,'' University of British Columbia Department of Computer Science Technical Report UBC CS 2000-05, June 10, 2000

    • A J H at C S dot U B C dot C A