Announced in September 2024. We look for 1) model checking specialists with aspiration for lattice- and category-theoretic abstract theories, or conversely, 2) category theorists with aspiration for efficient model checking algorithms.
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 seek a collaboration of
- concrete/algorithmic techniques for automated verification, such as graph-based model checking algorithms and automated software model checking, and
- abstract/structural theories such as lattice theory and category theory.
Through this collaboration, we aim not only at better automated verification algorithms, but also at extending the scope of automated verification to novel applications such as quantum systems, cyber-physical systems, and machine learning-based systems. We seek
- candidates with solid backgrounds in concrete automated verification techniques, with aspiration for abstract theories,
- or vice versa, i.e. those who have worked on abstract theories and aspire to use them in practical automated verification algorithms.
We believe that such a venture is beneficial for the candidates’ career building: their extended research portfolio will give them a unique technical edge and thus novel results in the short run, and also give them new sources of research problems in the long run. 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 pursue the collaboration between state-of-the-art algorithmic techniques for automated verification (e.g. those presented in CAV and TACAS) and abstract, structural/algebraic/categorical theories (those presented in LICS and FoSSaCS). The candidate will work closely with Prof. Ichiro Hasuo and other team members in Tokyo, as well as the collaborators overseas in Nijmegen, Aachen and Oxford. We seek both junior and senior researchers; the candidates may be granted an academic title (such as Project Assistant/Associate Professor).
Examples of the aforementioned collaboration between concrete algorithms and abstract theories are found in the following recent works.
- Abstract IC3/PDR [Kori et al., CAV’22 & CAV’23]. In this line of work, we take the IC3/PDR technique—a model-checking technique with a strong heuristic flavor with acclaimed performance in realistic benchmarks—and formulate its theoretical essences in lattice- and category-theoretic terms. This not only provides a high-level understanding of IC3/PDR (namely as a happy marriage between the Knaster-Tarski and Kleene theorems) but also produces efficient concrete model checking algorithms for a variety of systems (nondeterministic, probabilistic, quantitative, etc.).
- Compositional model checking [Watanabe et al., CAV’23, TACAS’24 & CAV’24]. Compositionality is a dream of every software scientist, but compositional model-checking algorithms have been rare. In this line of work, we use the theory of monoidal categories as a guidance and develop fully-automated and efficient compositional model checking algorithms. We use string diagrams—the “syntax” for monoidal categories—for system composition, and efficient algorithms are derived from categorical semantics that is, being algebra homomorphisms, compositional by construction. The categorical generality allows us to deal with a variety of systems (MCs, MDPs, mean payoff games, etc.); at the same time, we observe that the categorical approach goes along very well with concrete techniques in quantitative model checking such as guaranteed approximation and multi-objective optimization.
ESSENTIAL SKILLS AND REQUIREMENTS
- Motivated and dedicated. Able to work both independently and collaboratively
- Experience in concrete/algorithmic techniques in formal verification, or in abstract/algebraic theories of logic and systems
- Eagerness to broaden their research scope. Courage to learn and experiment with new techniques (Some theoreticians do not like the unpredictability of running experiments and waiting for their results. They are probably not suited for this position)
- Proven publication record
- Eagerness and experience in collaborative theoretical research
- 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
- Programming skills and experience
- (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.