Joe Leslie-Hurd


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 projects.


Selected Publications

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 LATEX by HEVEA.