ERATO Hasuo Metamathematics for Systems Design Project (ERATO MMSD) invites applications for a postdoc researcher. We aim to combine model checking and optimization metaheuristics, in order to scale formal verification techniques up to real-world industrial problems that are complex and black-box. We aim to do so, at the same time, in a way guided by solid meta-theoretical foundations such as those which we’ve presented in LICS and CAV. We thus explore new shapes of application of logic to modern software and systems. The position will be especially suited for those who have experience in model checking research and who wish to expand their research portfolio.
The candidate will work at National Institute of Informatics, Tokyo, Japan, and will pursue a novel extension of model checking techniques (temporal logic, automata theory) with optimization metaheuristics (evolutionary computation, stochastic optimization, statistical machine learning).
The goal is to overcome two major challenges that currently limit the applicability of formal verification techniques to real-world industrial systems, namely scalability and the absence of white-box models. In our endeavor towards the goal, we do not mind relying on testing, rather than exhaustive verification; this puts us somewhat closer to so-called lightweight formal methods.
That said, our theoretical development shall be nothing “lightweight.” We believe that there is a great theoretical depth here–we will explore the depth using logical, automata-theoretic, and/or categorical machinery. This theory of “lightweight” formal methods will significantly expand the current landscape of application of logic to software.
The position should be especially suited for model checking researchers who wish to expand their research portfolio. We find case studies in our industrial collaborations and seek applicability to those real-world problems (they are mostly from the manufacturing industry). At the same time, we seek rigorous logical/automata-theoretic/categorical foundations for the solutions we come up with–so our work stays well in the realm of the formal verification community. We work in an interdisciplinary environment, and the candidate will be constantly exposed to interaction with control theory, software engineering, automated driving, and category theory.
The candidate will work closely with Prof. Ichiro Hasuo and a few other team members. It is possible that the candidate be granted an academic title (such as Project Assistant/Associate Professor).
The following are some outcomes of our efforts so far. They are listed here in order to exemplify concrete topics. Note that the topics of these papers are diverse, and the candidate is not expected to follow all of them. A good match with one of them would suffice.
- Masaki Waga, Étienne André, Ichiro Hasuo: Symbolic Monitoring Against Specifications Parametric in Time and Data. CAV (1) 2019: 520-539. doi arXiv
(The topic is the theory of timed automata, which strikes a balance between theory and applicability.)
- Kittiphon Phalakarn, Toru Takisaka, Thomas Haas, Ichiro Hasuo: Widest Paths and Global Propagation in Bounded Value Iteration for Stochastic Games. CAV (2) 2020: 349-371 doi arXiv
(A work on a rather classic topic in formal verification, but the algorithm is approximate and highly scalable. The basic idea behind the algorithm has potential extensions, both theoretically and practically)
- Zhenya Zhang, Ichiro Hasuo, Paolo Arcaini: Multi-armed Bandits for Boolean Connectives in Hybrid System Falsification. CAV (1) 2019: 401-420. doi arXiv
(The work exploits logical structures to organize optimization metaheuristics on continuous domains.)
- Sota Sato, Atsuyoshi Saimen, Masaki Waga, Kenji Takao, Ichiro Hasuo: Hybrid System Falsification for Multiple-Constraint Parameter Synthesis: A Gas Turbine Case Study. FM 2021: 313-329. doi
(A real-world case study of logically structured optimization metaheuristics)
- Yuichi Komorida, Shin-ya Katsumata, Clemens Kupke, Jurriaan Rot, Ichiro Hasuo: Expressivity of Quantitative Modal Logics : Categorical Foundations via Codensity and Approximation. LICS 2021: 1-14. doi arXiv
(A categorical work, a potential foundation of our theory. If this paper is your closest match, please note that you are expected to be eager in working with optimization metaheuristics too.)
- Mayuko Kori, Natsuki Urabe, Shin-ya Katsumata, Kohei Suenaga, Ichiro Hasuo: The Lattice-Theoretic Essence of Property Directed Reachability Analysis. CoRR abs/2203.14261 (2022) arXiv
(Another categorical work, but with a big emphasis on implementation. You are expected to be familiar with or eager for both.)
ESSENTIAL SKILLS AND REQUIREMENTS
- Motivated, dedicated, and able to work both independently and collaboratively
- Proven publication record
- Familiarity with formal logic techniques (esp. temporal logic and automata theory)
- PhD degree (or be close to completion)
- Braveness to learn and experiment with new techniques (You will need it especially since optimization metaheuristics never guarantee good performance–you have to sit tight and wait for results)
- Eagerness and experience in collaborative theoretical research
- Must be able to communicate and work well with other team members
- Fluency in English, both orally and in paper writing
The following skills are not at all mandatory. They however will be a plus
- Familiarity with statistics and statistical machine learning
- Familiarity with optimization metaheuristics
- Familiarity with, or interest in, functional programming and category theory
- Tool development experience
- (Japanese language skills will be useful for everyday life, but not mandatory at all)
- This call was posted in April 2022. It will remain open until the position is filled.
- Annual gross salary: JPY 4,260,000 — 7,368,000 yearly, gross (depends on qualifications and experience).
- The contract is initially until the end of a fiscal year (March 31), with the possibility of extension (maximum until the project ends in March 2025).
- Our admin staff will provide support for moving, visa application, etc.
- Starting date: as early as possible
- Location: Tokyo, Japan (remote work from abroad is not allowed)
APPLICATIONS AND INQUIRIES
Applications should be sent to application_eratommsd [at] group-mmm.org, with the subject “ERATO Researcher Application.” Please include
- 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, provided that we find sufficient relevance in your application.
Inquiries should also be sent to application_eratommsd [at] group-mmm.org, with the subject “ERATO Researcher Inquiry.”
LIVING AND WORKING IN TOKYO
We have employed 10+ researchers and scientific programmers from abroad–see our list of members/former members. We have ample experience in supporting them in coming to and living in Tokyo.
Something comparable to those in Europe and Canada. This also explains our salary range (that should not put you off just because it is below the US standard).
The income tax is lighter than in many European countries. Try https://japantaxcalculator.com/ for an idea.
Tokyo is not an expensive city. On actual prices and availabilities you will find a lot of information sources on the web (including this). Some sample prices:
- An studio apartment, 30m2, 30min door-to-door to our Tokyo site: JPY 80,000 / month
- A 2-bedroom apartment, 40m2, 20min door-to-door to our Tokyo site: JPY 130,000 / month
- A 15-min metro ride: JPY 200
- A quick (but nice) Japanese set meal: JPY 600-1000
- An exquisite sushi set meal (which even locals rarely have 🙂 ): JPY 30,000
- A pint of beer: JPY 700
The working environment is totally in English, with more than half of the team coming from abroad. Japanese language skills will help everyday life, but one can definitely live without them, as we know from our colleagues’ experience.