[SMT-LIB] [Jobs] Intel is hiring formal-verification folks

[Levent Erkok]

[Apologies for slightly off-topic posting; but this job advert might
be interesting for the SMT-Lib community; our group's focus is on
automated-theorem proving using BDD/SAT/SMT based techniques; with
main emphasis on hardware.]


The group I work for at Intel has an opening for a recent
graduate (BS/MS/PhD) of a US institution.

We work within the product team responsible for the Xeon Phi many-core
processor which is used to build supercomputers.
See:http://en.wikipedia.org/wiki/Xeon_Phi

Our team focuses mainly on the floating-point arithmetic verification using
an internal STE based model checking tool called Forte, which is based on
the reFLect language, which itself is a descendant of ML. (With
lazy-evaluation default, and a baked-in BDD based equivalence checking
engine, which makes it supercool! Imagine Haskell with a built-in symbolic
simulation engine.) We also use Haskell for internal purposes as needed.
Our group has extensive freedom in the choice of tools we use.

We also work on a variety of non-arithmetic verification problems,
including cache coherence, ECC (error-detection/correction) algorithms,
instruction length decoders, to name a few. As part of our coherence work
we developed an open source explicit state distributed model checker called
PReach <https://bitbucket.org/jderick/preach/wiki/Home>.


Our group is based in Portland, OR, with one member in Santa Clara, CA.


Please let me know if you are, or you know anyone who might be interested
in this position. Feel free to forward this request.


-Levent.