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