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 independent research and regularly 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. He completed a Ph.D. at Cambridge University on the formal verification of probabilistic algorithms, and his work 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.
Joe Leslie-Hurd, Ph.D. 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. Until 2012 he was Formal Methods Lead at Galois, Inc., 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. He 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. Dr. Leslie-Hurd is an active member of the formal verification research community, having organized conferences in 2005, 2008 and 2013, given invited talks, and regularly appears on program committees and reviews papers for conferences and journals. Prior to joining Galois in 2007, Dr. Leslie-Hurd was a research fellow at Magdalen College, Oxford University. He studied at Cambridge University, receiving a Masters degree in Mathematics in 1997, and a Ph.D. in Computer Science in 2002.
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.