Postdoc position on Formal Verification for Zero-Trust IoT Systems at Kyoto University

by Atsushi Igarashi, Feb. 28, 2023

We are seeking a postdoc researcher, who works at Kyoto University, Japan for a project "Zero-Trust IoT Systems by Collaboration of Formal Verification and System Software" by Japan Science and Technology Agency. This is a great opportunity for programming language researchers who wish to pursue novel real-world applications.

* Project Description

The project aims at the construction of formally verified secure IoT

systems that follow the concept of "zero trust architecture", dubbed

ZT-IoT systems.  It consists of four research teams, and one of the

teams is led by Atsushi Igarashi, Kyoto University, investigating

applications of formal verification or programming language techniques

to the construction of secure IoT systems: more concretely, the design

and theory of security policy engines for ZT-IoT systems, including

the design of a language to describe security policies and policy

enforcement algorithms and the techniques for verifying policy

enforcement algorithms against given security policies.  Other team

members are Kohei Suenaga and Masaki Waga at Kyoto University.  

The team closely collaborates with another team, led by Taro Sekiyama,

National Institute of Informatics, Japan (NII), together with Ichiro

Hasuo and Shin-ya Katsumata at NII.

The appointment can start as early as May 2023 (the starting date is

negotiable).  The contract will initially run until the end of March

2024, with the possibility of annual renewal until the end of the

project, which is March 2027 at maximum.  The salary will be about

360,000–550,000 JPY/month.

Applicants should have a Ph.D. in computer science or related fields, and

have a strong background in formal verification and/or programming

language theory.  Due to the project's nature, they are required to have

strong interests in applying theory to practice; they should also be

(self-)motivated, dedicated, and able to work both independently and

collaboratively.  Strong communication skills in oral and written English

are required.

* Workplace

Kyoto University, Kyoto, Japan.

(Living costs in Japan are not very high nowadays.  An estimate is found here

* Applications and inquiries

Inquiries can be sent to application-zt-iot [at],

with the subject CREST Job Inquiry.  Feel free to ask us any questions on

relevance, topics, compensation, etc.  We will reply when we see enough


Applications should be made electronically via the following JREC-IN

Portal websites.

Please upload a pdf, including

- your brief CV,

- short description of research interests (can be very informal and short),

- the list of papers (a dblp or Google scholar link will do, for example),

- a couple of representative papers (in pdf), and

- (preferably) the contact of two references.

We will contact you for further material and an interview, provided that we

find sufficient relevance in your application.  Starting dates are

negotiable.  The positions will remain open until filled.


Atsushi Igarashi