http://www.gilith.com/
[email protected]

Experience

Formal Verification Engineer  2012–present
Intel Corporation  Portland, Oregon, USA

Applying formal verification tools to validate critical components of products, including cache coherency blocks, on-die mesh communication fabric, and floating point vector processing units. Technical work includes development of an automatic analysis of synthesized RTL to achieve full proofs of a new arithmetic datapath. Business tasks include planning and estimating formal verification execution efforts to support product development, as well as driving formal verification tool adoption by designers and validators through support/mentor/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 projects.

Education

• 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

Selected Publications

• Theo Drane, Samuel Coward, Mertcan Temel, and Joe Leslie-Hurd. On the systematic creation of faithfully rounded commutative truncated booth multipliers. In Proceedings of the 31st Symposium on Computer Arithmetic (ARITH 2024), pages 108–115. IEEE Computer Society, June 2024.
• 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.

Professional Service

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 L^AT_EX by H^EV^EA.