Jesse Bingham, Ph.D.

Welcome to my web page, which I designed myself using skills I picked up during a 1996 co-op job (joking aside, UVic has a great co-op program). All opinions on this page are that of the author, and are hence universally true.

I work for Intel, where I'm a member of the grandiosely titled: "Formal Verification Center of Expertise". Our mandate is to promote, enable, and support Formal Verification (FV) throughout the company. Many of these activities would undeniably be deemed unsexy from the perspective of the broader academic community, yet we march forth. This page serves to document the more research-oriented (and publicly sharable) work I've done, both at Intel and during my graduate studies at UBC Department of Computer Science. Here is a complete list of my publications; what follows is a summary of a selection of them. Please email me if you want to discuss any of these topics further, my email is jesse.d.binghum@intol.com, with the two spelling mistakes corrected.

• One of my roles at Intel is supporting data path FV. Thanks to the infamous FDIV bug, Intel hired many FVers during the mid 90s, and ever since datapaths have been a dominant focus of FV at Intel, with many smart folks working on these problems. As a late comer to the party, I'm excited when I find the odd niche where one can do something new. One such area is verifying designs with relative error specifications; a paper on our approach was presented at CAV 2014. I'm also working on using SAT solving in conjunction with traditional BDD-based symbolic simulation to ease the human burden required for decomposed proofs. I hope to publish something about this one day.

• Although pioneers in the field recently won a Turing award, model checking is not a panacea; unfortunately the inherent computational complexity bites us practitioners on a daily basis. Nevertheless, the most quaint form of model checking, explicit state model checking, sees some industrial usage on HW protocol models (and concurrent SW). Hence adding more oomph to these tools can never hurt. To this end, myself and collaborators at UBC and Intel developed a distributed version of the (now 2-decades old) Murphi model checker called PReach, which is available under a BSD license here.

  We made a cool extension to PReach to verify (absence of) deadlocks, which is a problem of great practical importance. Typically, FV papers and tools take "no deadlock" to mean that every reachable state has a successor. This is not the same as how computer architects think of deadlock: a cyclic dependency from which there is no escape. We characterized this notion by the CTL formula AGEFq. Here q is a state predicate capturing ``quiescence'', meaning there are no in-flight transactions. Rather than using the classical CTL model checking algorithm for this, which would involve a pre-image fixpoint computation from q, we developed a novel approach that uses a forward search to check for the EFq paths. This extension was published at CAV 2013 in this paper.

• An ongoing area of interest for me is the question of linking high-level, non-deterministic protocol models (expressed in e.g. TLA, Murphi, etc) to their RTL implementations. The holy grail of proving a suitable notion of "implementation" is difficult. During one project I worked on, we decided to write the requisite refinement map between the two systems and deploy the resulting refinement checks in the project's simulation environment, before even attempting a proof (a good strategy for hard FV problems in general IMHO). This work appeared as a short-paper at FMCAD 2009, which I believe nicely describes how one should best do this linkage.

• I completed a Ph.D. in formal verification with very little exposure to theorem proving. After a stint in a shortly-lived research group exposed me to HOL (higher-order logic) formalizations, I was hooked. You can prove (practically) anything given enough brain effort! And it's a beautiful language! I decided to immerse myself in some non-trivial proof and asked John Harrison to recommend a Mathematical theorem that had yet to be mechanized. The transcendence of e was one of his suggestions. I worked it in my free time over about 3 years, often going months without touching it, and ultimately wrote up the experience in a paper Formalizing a Proof that e is Transcendental. I'm also mentioned on Wiedijk's list of 100 theorems.