Fwd: [Coq-Club] Positions at a startup company, using Coq to prove hardware

[Andrés Sicard-Ramírez]

FYI.


---------- Forwarded message ----------
From: Adam Chlipala <ad...@csail.mit.edu>
Date: 6 August 2018 at 14:37
Subject: [Coq-Club] Positions at a startup company, using Coq to prove hardware
To: coq-...@inria.fr


I'm excited to announce opportunities for Coq hackers at the startup
company SiFive, for which I am a technical advisor.

Briefly, SiFive offers a platform to help their customers create new
hardware solutions, combining off-the-shelf components like CPUs with
application-specific components. They are very interested in
assurance about the correctness of such integration. Their library of
standard components is centered on the very cool open instruction set
RISC-V, which was created by the founders of the company. They are
located in Silicon Valley (California, USA).

SiFive is currently looking to hire a few Coq engineers to prove
correctness of processors and other crucial pieces of digital
hardware. I believe all or most of these components will be
open-source. The verification is being done using the Coq library
Kami that began its life in my group at MIT, partly under the umbrella
of the DeepSpec project. My former postdoc Murali Vijayaraghavan took
a job at SiFive to lead this effort.

I would encourage anyone interested in learning more to e-mail Murali.
Please be aware that these positions are only open to people with
nontrivial Coq experience, though experience with hardware engineering
is not required. (It all turns out to be functional programming,
anyway!) In applying, please start by summarizing your experience
using Coq, ideally to demonstrate correctness of (semi-)realistic
systems. The approximate bar is Coq familiarity at the level we'd
expect from doing a related master's thesis. However, there are also
internship opportunities that may be open to people with slightly less
Coq experience.

La información contenida en este correo electrónico está dirigida
únicamente a su destinatario y puede contener información
confidencial, material privilegiado o información protegida por
derecho de autor. Está prohibida cualquier copia, utilización,
indebida retención, modificación, difusión, distribución o
reproducción total o parcial. Si usted recibe este mensaje por error,
por favor contacte al remitente y elimínelo. La información aquí
contenida es responsabilidad exclusiva de su remitente por lo tanto la
Universidad EAFIT no se hace responsable de lo que el mensaje
contenga. The information contained in this email is addressed to its
recipient only and may contain confidential information, privileged
material or information protected by copyright. Its prohibited any
copy, use, improper retention, modification, dissemination,
distribution or total or partial reproduction. If you receive this
message by error, please contact the sender and delete it. The
information contained herein is the sole responsibility of the sender
therefore Universidad EAFIT is not responsible for what the message
contains.

--
Andrés