coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Freek Verbeek <freek AT vt.edu>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Postdoc Position VirginiaTech: x86-64 binary verification
- Date: Thu, 29 Mar 2018 09:35:58 -0400
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=freek AT vt.edu; spf=Pass smtp.mailfrom=freek AT vt.edu; spf=None smtp.helo=postmaster AT omr2.cc.vt.edu
- Ironport-phdr: 9a23:ZFnluRReejNfnJBZ1cXxFFVw8dpsv+yvbD5Q0YIujvd0So/mwa68bRKN2/xhgRfzUJnB7Loc0qyK6/umATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfb1/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/mHZhMJzkaxVvg6uqgdlzILIeoyYLuZycr/fcN4cWGFPXtxRVytEAo6kb4UPFfQOMvhbr4LgqFQBswG+ChKyC+zxyT9Dm3j73aMg0+s/Dw7G3xctH8wSsHjOstr6KboSXPmzwaLVwzvDaPZW1i386IjOah0hv+2MUahufsXM1EkiER7OgFaIqYH9Ij+Y0ucAv3KY4uZ+T+6jlm0qpg9rrjSy2Msgl5HFipwJxl3A7yl0w4Y4KcemREJlb9OoCoZcuiWeOoZwX8gsWXtnuDwgxb0DoZO7fDYFyJAgxxPHbPyHdpKI7gz5WOmNPTh0nmxleK6lixms7Eeg1/XwVsiy0FlUsipIisTAu3QO2hDJ6cWLVOFx8lqi1DuBzQzf9/9ILV0smareMZEhw7owlpQJsUTEGy/7gEv2jLWIeUo6+eil8PrnYqn8qpCCKoB0lxnyMr4ylcynHeQ4Lg8OUnCH9uS7zb3v5FH2QLFXjvItiaTZq5DbJcEDpqGjGQNV04Aj6wy+Dzi8ytgYk2MHfxp5f0eMiJGsMFXTKtj5C+2+ihKiimRF3ffDa5P7D5jOZkbOir3scLU1v0BGxQcw5c5DoZ9YF+dSc7rIRkbtuYmAXVcCOAuuzrO/UYQv5sYlQWuKR5ShHubXuF6M6PgoJrneepNTtTrgeaF8u6zeyEQhkFpYRpGHmIMNYSDqAOggLkmEMyK134UxVFwStw97d9TEzV2PVTkKOSS1WrhmoDowTpy6S4rPW9L1jQ==
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 AT 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 AT vt.edu) for any questions.
- [Coq-Club] Postdoc Position VirginiaTech: x86-64 binary verification, Freek Verbeek, 03/29/2018
Archive powered by MHonArc 2.6.18.