Jesse Bingham, Ph.D.
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.