Call for PhD Students

(For students in Japan, here is a more tailored description)

Basics

  • 5-year course (you enroll after BSc) or 3-year course (you enroll after MSc)
  • Affiliated with NII/SOKENDAI

Financial support

Baseline: ~ 100,000 JPY/month RA salary.
Max. ~ 400,000 JPY/month

  • RA salary becomes ~ 200,000 JPY/month once approved by NII (this happens typically when you get a first-authored publication)
  • This can be combined with JSPS DC Fellowship (~ 200,000 JPY/month. Many students of ours have succeeded in their application), and other similar fellowships
  • NB: you have to pay tuition fees (~ 50,000 JPY/month)

Environment

  • Big, diverse, and international team. See our list of members and former members.
  • Distincitively theoretical research, with motivations coming from real-world industry pains
  • Ample resources and admin support
  • Supervision by Ichiro Hasuo and other senior & early carrier staff members
  • Many successful students. List of theses

(Sample) Topics

Here are some sample topics (as of March 2022). Don’t worry too much about the desired qualifications–you can learn them after enrollment.

Categorical foundations of formal verification via coalgebras and fibrations

Fixed-point specifications (such as in LTL and modal \mu-calculus) have been conventionally studied in terms of finitary and combinatory structures (automata, games, etc.). These observations are recently being transferred to more abstract settings, opening up algorithms and proof methods for new application domains (esp. probabilistic, metric, etc.). There are a number of research questions waiting to be answered, both theoretical and algorithmic.

References: [Komorida, Katsumata, Hu, Klin, Hasuo, LICS’19], [Komorida, Katsumata, Kupke, Rot, Hasuo, LICS’21], [Kori, Hasuo, Katsumata, CONCUR’21], [Watanabe, Eberhart, Asada, Hasuo, MFPS’21]

Desired qualifications: familiarity with mathematical and abstract reasoning used in logic, lattice theory and (possibly) category theory

Logical guidance in optimization metaheuristics

Many real-world optimization problems have inherent logical and discrete structures, but many optimization metaheuristics (stochastic optimization, hill-climbing, evolutionary computation, etc.) do not make explicit use of such strucstructures. We have used hierarchical optimization frameworks where the upper logical layer guides the lower metaheuristics layer for efficiency and explainability. The goal is to push the idea further in other applications and theoretical foundations.

References: [Zhang, Hasuo, Arcaini, CAV’19], [Zhang, Ernst, Sedwards, Arcaini, Hasuo, EMSOFT’18]

Desired qualifications: familiarity with 1) formal logic, 2) optimization metaheuristics, 3) statistical machine learning

Combining local and global propagation in quantitative model checking

We are especially interested in value iteration, a family of approximate algorithms for quantitative model checking. Usual algorithms with only local propagation face certain challenges, and we have recently shown that those challenges are efficiently mitigated by mixing the right choice of global propagation. The goal is to push the idea further, to other problems, and to the formalization of theoretical foundations.

Reference: [Phalakarn, Takisaka, Haas, Hasuo, CAV’20]

Desired qualification: familiarity with model checking (see e.g. [Baier & Katoen ’08]), logic and automata. Familiarity with graph-theoretic algorithms is appreciated, too

Logical safety for automated driving

Responsibility-sensitive safety (RSS) is a recently proposed methodology for devising mathematically-guaranteed safety rules for automated driving. The candidate will work on its logical foundations and its application to various driving scenarios. The work is much like interactive theorem proving, but with unique theoretical challenges (e.g. continuous dynamics) and a hot application (automated driving).

References: [Shalev-Shwartz, Shammah, Shashua, arXiv’17] (our goal is to make the theory logically well-grounded)

Desired: familiarity with formal logic and interactive theorem proving, interest in bringing theory to practice

Practical formal verification of IoT security

In the context of the CREST ZT-IoT project, we aim at a practical proof-guided workflow for ensuring security of IoT systems. We do so by combining techniques for formal verification of security protocols with ideas from light-weight formal methods (model-based testing, runtime monitoring, etc.). We are in close collaboration with system software researchers who know a lot about, and will build, actual IoT systems.

Desired: familiarity with formal logic, and eagerness to learn from real-world applications and problems

Interested?

  • Contact Ichiro Hasuo i.hasuo <at> acm.org
  • When you do so, please include material that would speak for your capabilities and qualifications. Published/unpublished papers, reports, grades, a list of books and articles you have read, etc.
  • Please clarify which you’re thinking of: 5-year course (you enroll after BSc) or 3-year course (you enroll after MSc)
  • I will reply if the relevance is seen to be big enough