Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Postdoc Position VirginiaTech: x86-64 binary v...


view this post on Zulip Email Gateway (Aug 22 2022 at 16:52):

From: Freek Verbeek <freek@vt.edu>
A postdoctoral position is available with the Systems Software Research
Group (http://www.ssrg.ece.vt.edu) at Virginia Tech (https://vt.edu/) on a
project that is investigating verification of x86 machine code. The project
vision involves formalizing x86-64 semantics, decompiling program binaries,
and investigating techniques to reason about program behaviors, all inside
a theorem-prover.

Recent computer science or computer engineering PhD graduates with
background and expertise in theorem provers such as Isabelle/HOL, Coq, or
ACL2, and with an affinity for defining the formal semantics of languages
is sought. We seek candidates with a solid background in at least one of
the following topics:

Theorem proving / formal semantics
x86 architecture
Concurrency
Floating point semantics

Interested candidates should send a CV and cover letter to Dr. Freek
Verbeek (freek@vt.edu). Please indicate in your email that you are applying
for a postdoc position. The position is for one year, with strong
possibilities for additional years. The start date is flexible, but we aim
to fill the position as soon as possible. Please also contact Dr. Verbeek (
freek@vt.edu) for any questions.

view this post on Zulip Email Gateway (Aug 22 2022 at 19:53):

From: Freek Verbeek <freek@vt.edu>
A postdoctoral position is available with the Systems Software Research Group (http://www.ssrg.ece.vt.edu <http://www.ssrg.ece.vt.edu/>) at Virginia Tech (https://vt.edu/ <https://vt.edu/>) on a project that is investigating verification of x86 machine code. The project vision involves formalizing x86-64 semantics, decompiling program binaries, and investigating techniques to reason about program behaviors, all inside a theorem-prover.

Recent computer science or computer engineering PhD graduates with background and expertise in theorem provers such as Isabelle/HOL, Coq or ACL2, and with an affinity for defining the formal semantics of languages is sought. We seek candidates with a solid background in at least one of the following topics:

Theorem proving
x86 architecture
Concurrency

Interested candidates should send a CV and cover letter to Dr. Freek Verbeek (freek@vt.edu <mailto:freek@vt.edu>). Please indicate in your email that you are applying for a postdoc position. The position is for one year, with strong possibilities for additional years. The start date is flexible, but we aim to fill the position as soon as possible. Please also contact Dr. Verbeek (freek@vt.edu <mailto:freek@vt.edu>) for any questions.


Last updated: Apr 26 2024 at 04:17 UTC