<div dir="ltr"><div dir="ltr"><div>Hi all,</div><div><br>We are recruiting postdocs to work on formal methods and programming languages for the formal verification of TEE architectures, at National Institue of Informatics (NII(<a href="https://urldefense.com/v3/__https://www.nii.ac.jp/en/__;!!IBzWLUs!QPuj-hPaFaC9zxU0OifMv1wEZO06N9AAiIZotIHNdFOgmHcgLGyTqB38k4ue-z8E1j-_7V2dBdXroGY8pVN1ztER9ngIsZI$" target="_blank">https://www.nii.ac.jp/en/</a>) / Research Organization of Information and Systems (ROIS) (<a href="https://urldefense.com/v3/__https://www.rois.ac.jp/en/index.html__;!!IBzWLUs!QPuj-hPaFaC9zxU0OifMv1wEZO06N9AAiIZotIHNdFOgmHcgLGyTqB38k4ue-z8E1j-_7V2dBdXroGY8pVN1ztERaKqlHQo$" target="_blank">https://www.rois.ac.jp/en/index.html</a>), Tokyo, Japan.</div><div>We'd be grateful if you could spread the word to interested candidates.</div><div><br>This position is especially suited for programming language or program verification researchers seeking a new application domain at the intersection of systems programming, security, and hardware, with opportunities to develop new theory accordingly.<br><br>Relevant techniques (but not limited to) include:<br>- Proof assistants (e.g., Rocq and Agda)<br>- Type systems (especially for verification, like refinement and dependent type systems, or for systems programming, like C and Rust)<br>- Program logics (e.g., Separation Logic)<br>- Formal security verification<br>- Program refinement<br>- Program verifiers based on these techniques<br><br>Experience in modeling or verifying low-level languages (such as C, Rust, assembly languages, Verilog), systems software, or hardware will also be highly valued.<br><br>Please refer to the following webpage for the scope, details, and how to apply.<br>  <a href="https://urldefense.com/v3/__https://hackmd.io/@TaroSekiyama/H1ewltLsxx__;!!IBzWLUs!QPuj-hPaFaC9zxU0OifMv1wEZO06N9AAiIZotIHNdFOgmHcgLGyTqB38k4ue-z8E1j-_7V2dBdXroGY8pVN1ztERrWC4Avg$" target="_blank">https://hackmd.io/@TaroSekiyama/H1ewltLsxx</a></div><div><br>-- </div>Best regards,<br><div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature">Taro Sekiyama<br><a href="https://urldefense.com/v3/__https://skymountain.github.io/__;!!IBzWLUs!QPuj-hPaFaC9zxU0OifMv1wEZO06N9AAiIZotIHNdFOgmHcgLGyTqB38k4ue-z8E1j-_7V2dBdXroGY8pVN1ztERV8BGXLA$" target="_blank">https://skymountain.github.io/</a></div></div>
</div>