Component Design Engineer 2012–present
Intel Corporation Portland, Oregon, USA
Applying formal verification tools to critical components of many-core
processors, including vector processing with floating point
arithmetic. Technical work includes development of an automatic
analysis of synthesized RTL to achieve full proofs of a new arithmetic
datapath. Business tasks include proposing and estimating formal
verification efforts to support early-stage projects, as well as
driving formal verification tool adoption by product group designers
and validators through support/presentation/hiring activities.
Formal Methods Lead 2007–2012
Galois, Inc. Portland, Oregon, USA
Engineering and business roles in high assurance software research.
Business tasks include proposal writing, hiring, budgeting and project
management. Engineering work includes development of automatic static
analysis tools for C and Android, designing a policy language to model
information flow across security domains, and formal verification of
elliptic curve cryptography.
Fellow in Computation 2003–2007
Magdalen College Oxford University, UK
Research in formal verification techniques, focusing on deploying
advanced proof techniques as automatic tactics in interactive theorem
provers. Teaching experience includes Ph.D. examination, lecturing
and advising at the graduate and undergraduate level, small group
teaching, interviewing students.
Postdoctoral Research Associate 2001–2003
Computer Laboratory Cambridge University, UK
Research in Fully Expansive Proof and Algorithmic Verification:
using a higher order logic theorem prover as a platform to implement a
verifying compiler from Property Specification Language (PSL)
assertions to Verilog hardware monitors. Teaching experience includes
undergraduate lecturing, small group teaching and advising final year
- Cambridge University, 2002. Ph.D. in Computer Science
Dissertation: Formal Verification of Probabilistic Algorithms.
- Cambridge University, 1997. Masters in Mathematics
- Cambridge University, 1996. B.A. (Hons) in Mathematics
- Warren E. Ferguson, Jesse Bingham, Levent Erkok, John R. Harrison, and Joe Leslie-Hurd. Digit serial methods with applications to division and square root. IEEE Transactions on Computers, 67(3):449–456, March 2018.
- Jesse Bingham and Joe Leslie-Hurd. Verifying relative error bounds using symbolic simulation. In Armin Biere and Roderick Bloem, editors, Proceedings of the 26th International Conference on Computer Aided Verification (CAV 2014), volume 8559 of Lecture Notes in Computer Science, pages 277–292. Springer, July 2014.
- Joe Leslie-Hurd. Maintaining verified software. In Chung-chieh Shan, editor, Haskell ’13: Proceedings of the 2013 ACM SIGPLAN symposium on Haskell, pages 71–80. ACM, September 2013.
- Joe Hurd. The OpenTheory standard theory library. In Mihaela Bobaru, Klaus Havelund, Gerard J. Holzmann, and Rajeev Joshi, editors, Third International Symposium on NASA Formal Methods (NFM 2011), volume 6617 of Lecture Notes in Computer Science, pages 177–191. Springer, April 2011.
- 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. Springer, May 2010.
- 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.
- 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. Springer, August 2002.
- 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. Springer, July 2002.
Conferences Organized the FMCAD 2013, TTVSI
2008 and TPHOLs 2005 conferences; served on the program
committee of TPHOLs, ITP and NFM conferences.
Reviewing Served on an NSF panel; Ph.D. examiner at the
University of New South Wales and Ȧbo Akademi; review papers for
many formal verification conferences and journals.
Speaking Invited speaker at SVARM 2013,
SHARCS 2012, SSV 2010 and workshops of FLoC 2010
and LPAR 2005; presented papers at many international conferences
and research seminars.
Development OpenTheory, a package management
system for higher order logic theories; Metis, an automatic
theorem prover for first order logic; plus many theories and proof
tools in the HOL4 interactive theorem prover. All
these systems are open source with commercial-friendly licenses.
This document was translated from LATEX by