About - Gilith

Joe Leslie-Hurd
Formal Verification Engineer at Intel Corporation
Portland, Oregon, USA

Contact Details

Mailing Address:

Joe Leslie-Hurd
Intel Corporation
Mail Stop JF4-419
2111 NE 25th Ave
Hillsboro, OR 97124, USA

Professional Biographies

Joe is an engineer at Intel Corporation in Portland, Oregon, where he verifies critical components of many-core processors. Before that, he worked at Galois, Inc. where he used functional programming languages to construct correctness proofs of software. He studied at Cambridge University, receiving degrees in mathematics and then computer science as he made the realization that it was more fun to program computers to find proofs than to do them by hand. In his free time Joe contributes to open source projects, carries out research and gives talks to audiences at all levels.

Joe Leslie-Hurd is a Formal Verification Engineer at Intel Corporation in Portland, Oregon. His work focuses on verifying critical components of many-core processors, including vector processing with floating point arithmetic. Before that he was Formal Methods Lead at Galois, Inc., where he applied rigorous semantic techniques to design and analyze security-critical software. Joe completed a Ph.D. at Cambridge University on the formal verification of probabilistic algorithms, and since then has developed a package management system and automatic theorem prover for higher order logic. He also created the world's first formally verified chess endgame database.

Joe Leslie-Hurd is a Formal Verification Engineer at Intel Corporation in Portland, Oregon. Since joining in 2012 his work has focused on verifying critical components of many-core processors, including vector processing with floating point arithmetic. Dr. Leslie-Hurd was Formal Methods Lead at Galois, Inc. from 2007–2012, where he applied techniques founded on formal semantics to design and analyze security-critical software. He has over 15 years experience formally verifying the correctness of complex software, including probabilistic programs, elliptic curve cryptography and game tree analysis algorithms. Dr. Leslie-Hurd is the developer of Metis, an automatic theorem prover for first order logic, and coordinates the OpenTheory project, a package management system for higher order logic theories. He is an active member of the formal verification research community, having organized conferences in 2005, 2008 and 2013, and serves on program committees and reviews papers for many conferences and journals. Dr. Leslie-Hurd was a research fellow at Magdalen College, Oxford University from 2003–2007. He studied at Cambridge University, receiving a Masters in Mathematics in 1997, and a Ph.D. in Computer Science in 2002.

Curriculum Vitae

In HTML and PDF formats. Also: a full list of publications in HTML and PDF formats.

Personal Biography

The eldest of three brothers, I grew up in the Bath end of Somerset: a county in the south west of England. My first nine years were spent in the tiny village of Cranmore, and then my family moved to the nearby town of Frome. There I attended Frome College and took up chess to while away the lunchtimes. I completed my studies in Cambridge, and then worked for a time in the university Computer Laboratory while living in the village of Girton. I continued my research in Oxford, taking up go to while away the evenings, and then moved into industry in Portland, Oregon.

What's in a Name?

J. R. R. Tolkien was a professor of philology at Oxford University, and used his skills to devise languages spoken in his fantasy world of Middle-earth. The word gilith means "outer space" in Sindarin, a language spoken by elves. Here is a poem I like from the Lord of the Rings:

All that is gold does not glitter,
Not all those who wander are lost;
The old that is strong does not wither,
Deep roots are not reached by the frost.

From the ashes a fire shall be woken,
A light from the shadows shall spring;
Renewed shall be blade that was broken,
The crownless again shall be king.