Joe Hurd

Joe Hurd

Contact

Research and Engineering
Office: 503.626.6616 x152
Email: joe (at) galois (dot) com
Webpage: http://www.gilith.com/
Twitter: http://twitter.com/gilith
LinkedIn: http://www.linkedin.com/pub/joe-hurd/b/b2b/956

At Galois

I work on high assurance compiler technology for security applications, which ties in with my interest in formal verification and higher order logic theorem provers. I lead the Formal Methods research program at Galois and also give talks to promote interest in mathematics and computer science:

My Background

I completed a Ph.D. at the University of Cambridge on the formal verification of probabilistic programs in 2002, and my research since has included: developing a package management system for higher order logic theories; applying automatic proof techniques for first order logic; and creating the world's first formally verified chess endgame database.

Publications

My website contains a complete list of my publications.

  • David Burke, Joe Hurd, John Launchbury, and Aaron Tomb. Trust relationship modeling for software assurance. In Proceedings of the 7th International Workshop on Formal Aspects of Security & Trust (FAST 2010), September 2010.
  • Joe Hurd. Composable packages for higher order logic theories. In M. Aderhold, S. Autexier, and H. Mantel, editors, Proceedings of the 6th International Verification Workshop (VERIFY 2010), July 2010.
  • Joe Hurd and Guy Haworth. Data Assurance in Opaque Computations. In H. Jaap Van den Herik and Pieter Spronck, editors, Advances in Computer Games, 12th International Conference (ACG 2009), volume 6048 of Lecture Notes in Computer Science, pages 221–231, Pamplona, Spain. Springer, May 2010.
  • Joe Hurd. OpenTheory: Package management for higher order logic theories. In Gabriel Dos Reis and Laurent Théry, editors, PLMMS '09: Proceedings of the ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems, pages 31–37, Munich, Germany, August 2009. ACM.
  • Joe Hurd. Proof pearl: The termination analysis of TERMINATOR. In Klaus Schneider and Jens Brandt, editors, 20th International Conference on Theorem Proving in Higher Order Logics: TPHOLs 2007, volume 4732 of Lecture Notes in Computer Science, pages 151–156, Kaiserslautern, Germany, September 2007. Springer.
  • Jianjun Duan, Joe Hurd, Guodong Li, Scott Owens, Konrad Slind, and Junxing Zhang. Functional correctness proofs of encryption algorithms. In Geoff Sutcliffe and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, 12th International Conference (LPAR 2005), volume 3835 of Lecture Notes in Artificial Intelligence, pages 519–533, Montego Bay, Jamaica, December 2005. Springer.
  • Joe Hurd, Annabelle McIver, and Carroll Morgan. Probabilistic guarded commands mechanized in HOL. Theoretical Computer Science, 346:96–112, November 2005.
  • Mike Gordon, Joe Hurd, and Konrad Slind. Executing the formal semantics of the Accellera Property Specification Language by mechanised theorem proving. In Daniel Geist and Enrico Tronci, editors, Correct Hardware Design and Verification Methods (CHARME 2003), volume 2860 of Lecture Notes in Computer Science, pages 200–215. Springer, October 2003.
  • Joe Hurd. First-order proof tactics in higher-order logic theorem provers. In Myla Archer, Ben Di Vito, and César Muñoz, editors, Design and Application of Strategies/Tactics in Higher Order Logics (STRATA 2003), number NASA/CP-2003-212448 in NASA Technical Reports, pages 56–68, September 2003.
  • Konrad Slind and Joe Hurd. Applications of polytypism in theorem proving. In David Basin and Burkhart Wolff, editors, 16th International Conference on Theorem Proving in Higher Order Logics: TPHOLs 2003, volume 2758 of Lecture Notes in Computer Science, pages 103–119, Rome, Italy, September 2003. Springer.
  • Joe Hurd. Verification of the Miller-Rabin probabilistic primality test. Journal of Logic and Algebraic Programming, 50(1–2):3–21, May–August 2003. Special issue on Probabilistic Techniques for the Design and Analysis of Systems.
  • Joe Hurd. A formal approach to probabilistic termination. In Víctor A. Carreño, César A. Muñoz, and Sofiène Tahar, editors, 15th International Conference on Theorem Proving in Higher Order Logics: TPHOLs 2002, volume 2410 of Lecture Notes in Computer Science, pages 230–245, Hampton, VA, USA, August 2002. Springer.
  • Joe Hurd. An LCF-style interface between HOL and first-order logic. In Andrei Voronkov, editor, Proceedings of the 18th International Conference on Automated Deduction (CADE-18), volume 2392 of Lecture Notes in Artificial Intelligence, pages 134–138, Copenhagen, Denmark, July 2002. Springer.
  • Joe Hurd. Predicate subtyping with predicate sets. In Richard J. Boulton and Paul B. Jackson, editors, 14th International Conference on Theorem Proving in Higher Order Logics: TPHOLs 2001, volume 2152 of Lecture Notes in Computer Science, pages 265–280, Edinburgh, Scotland, September 2001. Springer.
  • Joe Hurd. Congruence classes with logic variables. Logic Journal of the IGPL, 9(1):59–75, January 2001.
  • Joe Hurd. Integrating Gandalf and HOL. In Yves Bertot, Gilles Dowek, André Hirschowitz, Christine Paulin, and Laurent Théry, editors, Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs '99, volume 1690 of Lecture Notes in Computer Science, pages 311–321, Nice, France, September 1999. Springer.