coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Vilhelm Sjöberg <vilhelm.sjoberg AT certik.io>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Research Internships using Coq at CertiK
- Date: Wed, 24 Feb 2021 15:12:57 -0500
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=vilhelm.sjoberg AT certik.io; spf=Pass smtp.mailfrom=vilhelm.sjoberg AT certik.org; spf=None smtp.helo=postmaster AT mail-pg1-f173.google.com
- Ironport-phdr: 9a23:6GN8GhyEi+XykfLXCy+O+j09IxM/srCxBDY+r6Qd2+wUIJqq85mqBkHD//Il1AaPAdyKraIbwLKM+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxhMiTanYr5/Lhq6oRnPusILnYZsN6E9xwfTrHBVYepW32RoJVySnxb4+Mi9+YNo/jpTtfw86cNOSL32cKskQ7NWCjQmKH0169bwtRbfVwuP52ATXXsQnxFVHgXK9hD6XpP2sivnqupw3TSRMMPqQbwoXzmp8qFmQwLqhigaLT406G7YhMx+gqxYvRyvuQBwzpXOb42JLvdzZL/Rcc8YSGdHQ81fVzZBAoS5b4YXAOUBPOJYr4njqFsKqBuxHRSiBOHp0jBTmHD2x6I62PkmHAHY3QwgG9IOv2rQrNXwLqsSSuK1zK7TwjrddfNW1izw55TWfRA7vfGMXLFwfdDQyUkoDg7IiEibpoP5MT2PzOsNr3Sb4PR6VeKpk2MqrwB8rzeyy8oylIXEgpwYxkzY+Ch43Ys7K8C1RU17b9O4H5VdqS6UO5VqT88/TW9mtic3xqMItJO4YCQEyIoqyhjCYPKJdIiI5wjsVOeXITpggHJqZqy/iAio8US61uL8Uc+520tJoCpditTAqGwB2hjJ5sWESvZx5Fmt1SuP2gzJ9+1JI045mKzGIJA72LEwjIAcsUHbEy/2hkr2iKiWe10h+uey6uTnZqzqpoeTN4Npkw3+PLkil86xDOgiPQgOWG+b+eu41LL950H2XLJKjvgunqnYtpDVO9gbq7anDwNJ1osv8RWyAje83NgGgHUKLEhJdA+FgoXnI13OJer3Dfa7g1SiijdrwPXGM6X/ApXMKnjDkKnufbJ460JG0wozz9df6IlKBbEbL/L+QVP+u8LCDh8lMgy0wPzrCNJn1oMRQW6PGLOWMLvOsV+U4eIiO/WDZIgMuDrkN/cl4+PugmQilF8Gfaip2IMXZ2qiEvRnJUWZe3vsjc0bHWcEpAptBNDt3VaFSHtYY2u4d6M6/DAyToy8XqnZQYX4vr2F3Cq/G6ptZP5MB0qDWSP2doGEVvMJLjmQJcVsiDMsXrW7V44ikxCp4lypg4F7J/bZr3VL/ano08J4srWKxEMCsAdsBsHY6FmjCmR9n2cGXTgzhfotqkFn1laAl69ijK4BTIEB17ZySg4/cKXk4al6BtT1AFyTe96ITBO+TYzjD2huFZQ+xNgBZ0s7ENKn3Eiag3iaRoQNnrnOP6Qat7rG1iGodc1w0WrH1+8giAt+Tw==
CertiK is a world-leading cybersecurity firm based in NYC that focuses on auditing smart contracts, blockchain platforms and system software. It was founded by prof. Ronghui Gu (Columbia) and prof. Zhong Shao (Yale), drawing on their research about formal verification.
In-house, CertiK is developing an operating system kernel (CertiKOS) and a certified compiler (DeepSEA), both of them verified using the Coq proof assistant. Together with commercial clients we are using both Coq and SMT-based tools to verify software written in Rust and Go. We are looking for interns to help take our work to the next level.
Available projects include: verifying hypervisors and programming language runtimes written in Rust; adding new language features, optimizations, or new verified backends to DeepSEA; building new formal verification tools for Go and Solidity; and more.
The internship is suitable for current master/phd students, or strong undergraduates looking for research experience. Because of the current Covid-19 epidemic, these positions are completely remote. You should be familiar with one of the following areas:
Formal verification using an interactive proof assistant (e.g. from reading the Software Foundations textbook or similar).
[Preferred] Experience with non-trivial projects written in Coq. Proficient in Rust.
OR
Familiar with compiler implementation (e.g. from taking an Compilers class), and experience with functional programming (e.g. Ocaml, Gallina).
[Preferred] Previous experience working on a compiler; or experience specifying programming languages using operational semantics; or experience working with WASM, LLVM, or EVM.
OR
Experience with SMT-based theorem proving systems (Z3, Boogie, Why3, etc) or model checkers.
[Preferred] Previous experience building verification tools for programming languages.
Please send applications via https://jobs.lever.co/certik/d961cd21-44cf-4757-bc72-cc742fb7da2e
Best regards,
Vilhelm Sjöberg
In-house, CertiK is developing an operating system kernel (CertiKOS) and a certified compiler (DeepSEA), both of them verified using the Coq proof assistant. Together with commercial clients we are using both Coq and SMT-based tools to verify software written in Rust and Go. We are looking for interns to help take our work to the next level.
Available projects include: verifying hypervisors and programming language runtimes written in Rust; adding new language features, optimizations, or new verified backends to DeepSEA; building new formal verification tools for Go and Solidity; and more.
The internship is suitable for current master/phd students, or strong undergraduates looking for research experience. Because of the current Covid-19 epidemic, these positions are completely remote. You should be familiar with one of the following areas:
Formal verification using an interactive proof assistant (e.g. from reading the Software Foundations textbook or similar).
[Preferred] Experience with non-trivial projects written in Coq. Proficient in Rust.
OR
Familiar with compiler implementation (e.g. from taking an Compilers class), and experience with functional programming (e.g. Ocaml, Gallina).
[Preferred] Previous experience working on a compiler; or experience specifying programming languages using operational semantics; or experience working with WASM, LLVM, or EVM.
OR
Experience with SMT-based theorem proving systems (Z3, Boogie, Why3, etc) or model checkers.
[Preferred] Previous experience building verification tools for programming languages.
Please send applications via https://jobs.lever.co/certik/d961cd21-44cf-4757-bc72-cc742fb7da2e
Best regards,
Vilhelm Sjöberg
- [Coq-Club] Research Internships using Coq at CertiK, Vilhelm Sjöberg, 02/24/2021
Archive powered by MHonArc 2.6.19+.