Postdoc positions at NII / ROIS Tokyo in formal verification of secure systems

--===============2923059795128184123==
Content-Type: multipart/alternative; boundary="000000000000f54a49063ee6928f"

--000000000000f54a49063ee6928f
Content-Type: text/plain; charset="UTF-8"

Hi all,

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) (https://www.nii.ac.jp/en/) / Research
Organization of Information and Systems (ROIS) (
https://www.rois.ac.jp/en/index.html), Tokyo, Japan.
We'd be grateful if you could spread the word to interested candidates.

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.

Relevant techniques (but not limited to) include:
- Proof assistants (e.g., Rocq and Agda)
- Type systems (especially for verification, like refinement and dependent
type systems, or for systems programming, like C and Rust)
- Program logics (e.g., Separation Logic)
- Formal security verification
- Program refinement
- Program verifiers based on these techniques

Experience in modeling or verifying low-level languages (such as C, Rust,
assembly languages, Verilog), systems software, or hardware will also be
highly valued.

Please refer to the following webpage for the scope, details, and how to
apply.
  https://hackmd.io/@TaroSekiyama/H1ewltLsxx

Best regards,
Taro Sekiyama
National Institue of Informatics
https://skymountain.github.io

--000000000000f54a49063ee6928f
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr"><div>Hi all,</div><div><br>We are recruiting postdocs to w=
ork on formal methods and programming languages for the formal verification=
 of TEE architectures, at National Institue of Informatics (NII) (<a href=
=3D"https://www.nii.ac.jp/en/" target=3D"_blank">https://www.nii.ac.jp/en/<=
/a>) / Research Organization of Information and Systems (ROIS) (<a href=3D"=
https://www.rois.ac.jp/en/index.html" target=3D"_blank">https://www.rois.ac=
.jp/en/index.html</a>), Tokyo, Japan.</div><div>We&#39;d be grateful if you=
 could spread the word to interested candidates.</div><div><br>This positio=
n is especially suited for programming language or program verification res=
earchers seeking a new application domain at the intersection of systems pr=
ogramming, 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 v=
erification, like refinement and dependent type systems, or for systems pro=
gramming, like C and Rust)<br>- Program logics (e.g., Separation Logic)<br>=
- Formal security verification<br>- Program refinement<br>- Program verifie=
rs based on these techniques<br><br>Experience in modeling or verifying low=
-level languages (such as C, Rust, assembly languages, Verilog), systems so=
ftware, or hardware will also be highly valued.<br><br>Please refer to the =
following webpage for the scope, details, and how to apply.<br>=C2=A0=C2=A0=
<a href=3D"https://hackmd.io/@TaroSekiyama/H1ewltLsxx" target=3D"_blank">ht=
tps://hackmd.io/@TaroSekiyama/H1ewltLsxx</a></div><font color=3D"#888888"><=
div><br></div>Best regards,<br><div dir=3D"ltr" class=3D"gmail_signature">T=
aro Sekiyama<br>National Institue of Informatics<br><a href=3D"https://skym=
ountain.github.io/" target=3D"_blank">https://skymountain.github.io</a></di=
v></font></div>

--000000000000f54a49063ee6928f--

--===============2923059795128184123==
Content-Type: text/plain; charset="us-ascii"
MIME-Version: 1.0
Content-Transfer-Encoding: 7bit
Content-Disposition: inline

_______________________________________________
Haskell mailing list -- [email protected]
To unsubscribe send an email to [email protected]

--===============2923059795128184123==--