Announced in September 2024. We look for formal verification specialists (theorem proving or model checking) with aspiration to take up real-world problems.
Group MMM at National Institute of Informatics, Tokyo, Japan, invites applications for postdoc and senior researcher positions. In this opening (see also these positions which are open at the same time), we tackle the methodological challenge that logical methods in software science are currently facing: the absence of mathematical models of systems. To state and prove a safety theorem, one has to first define all the notions involved, and this amounts to modeling. Without models, there are no definitions, so no theorems to prove. This challenge is the most notable with cyber-physical and ML/AI systems.
Therefore, in our project, we pursue a re-invention of the role of logic, namely as an accountable, interpretable, traceable and transparent interface between ICT and society.
Specifically, we pursue such a role of formal logic by
- carefully matching logical/technical seeds and social/applicational needs,
- flexibly choosing the goal of our technique (e.g. efficient testing rather than formal verification), and
- extending logical techniques to cater to such extended goals, minding their effectiveness and generality.
We seek candidates
- who have strong technical backgrounds in deductive verification and/or model checking, and
- who aspire to tackle real-world problems, especially in the cyber-physical and ML/AI domains.
An ideal candidate is an open-minded theoretician who believes that diving into application domains should pay off in the long run (this is very probably the case also in the short run). Our unique environment that mixes logical theories, categorical metatheories, and active industry collaboration (with manufacturing and automotive companies) provides many opportunities. The position will broaden the candidate’s research portfolio and boost their career. We look forward to applications from junior and senior researchers with aspiring minds.
JST ASPIRE Project
The positions are for the JST ASPIRE project “Network of Software Studies towards Social Trust in Information Technologies.” The project’s PI is Ichiro Hasuo, and it collaborates with, as overseas co-PIs, Bart Jacobs (Radboud U, Nijmegen, NL), Joost-Pieter Katoen (RWTH Aachen, DE), and Sam Staton (U Oxford, UK). Collaboration with their groups is pursued under mutual visits.
In the JST ASPIRE project, we aim to establish a general interface between society and emerging information technologies such as automated driving and generative AI. For human-centric adoption and development of those information technologies–-they are intrusive in the sense that they necessarily incur changes of the shape of our current society—transparent, explainable, and accountable safety guarantees are vital. We use cutting-edge software science techniques for this purpose, from abstract, mathematical, and categorical to concrete, heuristic, and algorithmic.
Job Description
The candidate will tackle the aforementioned challenge (absence of formal models), working in two directions:
- to dive into an application domain, listening to the practitioners, identifying their essential needs, and formalizing problems therein, and
- to extend logical techniques—deductive verification, model checking, etc.—to cater to those problems and needs.
The challenge of the absence of models is the most common in cyber-physical and AI/ML systems (see the figure below). These are also the domains in which we work with industry the most; therefore it is likely that the candidate work on one of those.
Examples of our efforts towards “logic as an accountable interface between ICT and society” are found in the following recent works.
- Formal verification of safety of automated driving vehicles [Hasuo et al., IEEE Trans. Intell. Vehicles ’23; Eberhart et al., IV’23; Haydon et al., ITSC’23]. Formal safety verification of automated vehicles, in the conventional sense of “all the way up from the first principle,” is impossible due to the lack of models. Following the idea of RSS [Shalev-Shwartz et al. ‘17], we instead pursue contract-based safety proofs, where safety is proved conditionally on behavioral responsibility contracts imposed on each traffic participant.
In fact, such behavioral contracts—they can be called “mathematical traffic laws”—are what is needed by society. Firstly, the current road traffic system is designed in such a way that accidents cannot be completely avoided (a drunk person can throw themselves in front of a car)—what matters is the liability attribution when an accident happens. Our behavioral contracts explicate who is responsible for what. Secondly, our “mathematical traffic laws” can be implemented and retrofitted to existing controllers as a safety envelope, providing safe controllers and easing the real-world adoption of automated driving cars. - Model-free formal methods. In this line of work, we emphasize the role of formal specifications—the other main character of the conventional methodology of formal verification besides system models. A number of benefits can be brought about even with formal specifications alone, especially in the cyber-physical domain.
Concretely, such benefits can be- Automated and efficient tools for monitoring, runtime verification, testing and optimization [Waga et al., CAV’19; Zhang et al., CAV’21; Sato et al., FM’21], and
- Explicating contracts among systems and society, removing ambiguities and easing decision making [Reimann, Mansion et al., SAC’24].
ESSENTIAL SKILLS AND REQUIREMENTS
- Motivated and dedicated. Able to work both independently and collaboratively
- Strong technical backgrounds in formal verification (deductive verification or model checking)
- Eagerness to broaden their research scope. Courage to dive into application domains and listen to practitioners’ needs
- Proven publication record
- PhD degree (or be close to completion)
- Eager to communicate and work with other team members
- Positive and easy-going
- Fluency in English, both orally and in paper writing
DESIRABLE SKILLS
The following skills are not at all mandatory. They however will be a plus
- Experience in industry collaboration
- (Japanese language skills will be useful for everyday life, but not mandatory at all)
PRACTICAL
- This call was posted in September 2024. It will remain open until the positions are filled. (There is another researcher call that we are currently advertising. The current call may be closed early if we have good candidates for this other call.)
- Annual gross salary: starting at JPY 4,260,000 yearly, gross. It depends on qualifications and experience; for senior researchers, it can go quite high
- 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 2029).
- Our admin staff will provide support for moving, visa application, etc.
- Starting date: as early as possible
- Location: Tokyo, Japan (you will need to move there)
APPLICATIONS AND INQUIRIES
Applications should be sent to application_eratommsd [at] group-mmm.org, with the subject “ASPIRE Researcher Application (Abstract and Concrete Formal Verification).” 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
- the contact of two or more references (you can also send us their recommendation letters).
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 “ASPIRE Researcher Inquiry (Abstract and Concrete Formal Verification).”
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.
SOCIAL BENEFITS
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.
PRICES
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 90,000 / month
- A 2-bedroom apartment, 40m2, 20min door-to-door to our Tokyo site: JPY 150,000 / month
- A 15-min metro ride: JPY 200
- A quick (but nice) Japanese set meal: JPY 800-1200
- An exquisite sushi set meal (which even locals rarely have 🙂 ): JPY 30,000
- A pint of beer: JPY 800
APARTMENTS
You can easily find an apartment using the following websites: www.sabbaticalhomes.com, www.sakura-house.com/en, gaijinpot.com, and others. (We have a more comprehensive list)
LANGUAGE
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.