Jesse Bingham, Ph.D.
My name's Jesse and my primary area of research/development/trench warfare is formal verification. I was originally attracted to this area since I was a fan of Theoretical Computer Science and Math, and it appeared that formal verification was an area with both theoretical depth and practical use. Ironically, my primary PhD supervisor, Alan Hu, held/holds the commendable belief that formal verification research should focus on the practical, rather than fall victim to being theory-for-theory's-sake. Adding a second level of irony, he was gracious enough to allow me to pursue a highly theoretical dissertation. And the final twist is that for the past few years I've been working at Intel in formal verification, where practicality for formal verification folk is a necessity for job preservation.

Anyway, if you look at my publications, you'll see that I've dabbled in several areas of formal verification research: parameterized model checking, SAT solving, bounded model checking, software verification, memory model verification, and decision procedures.

Currently, my pursuits can be categorized roughly in two bins: things I get paid for, and things I don't get paid for. For the former, I'm working on the problem of connecting register transfer level implementations of protocol components with their high level models. A glimpse of that work can be found in a recent talk I gave as an invited lecture for Erik Seligman's course at Portland State University. I'm also ramping up on a methodology developed at Intel for verifying arithmetic circuits, in particular fused multiply-add instructions. For work of the non-paid variety , I'm really excited about theorem proving and am proving a certain famous mathematical theorem that has yet to be mechanized in HOL Light.

My geeky brother also choose to hit the snooze button of life (grad school) with a double-smackdown.

There's probably very few humans that are both Nomeansno fans and users of HOL Light. In fact I just might be the only one. Therefore, I'm in a unique position to inform the world that Tom Holliston, guitarist for Nomeansno and British Columbia punk rock legend, and John Harrison, fellow Inteller and inventer of Hol light, are twin brothers separated at birth!.