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