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
_______________________________________________
Haskell mailing list -- haskell@haskell.org
To unsubscribe send an email to haskell-le...@haskell.org

Reply via email to