Open Positions in Tokyo: Formal Methods and Cyber-Physical Systems
Dear colleagues,
For our 5-year research project (ERATO MMSD, Metamathematics for Systems Design) we are looking for senior researchers and postdocs (10+ positions in total and several are still open), together with research assistants (PhD students) and internship students.
This broad project aims to extend the realm of formal methods from software to cyber-physical systems (CPS), with particular emphases on logical/categorical metatheories and industrial application esp. in automotive industry. The project covers diverse areas that include:
formal methods, programming languages, control theory, control engineering, software science, software engineering, machine learning, numerical optimization, user interface, mathematical logic and category theory.
About Project:
ERATO MMSD is a JST-funded 5.5-year project (via the ERATO funding scheme) dedicated to Metamathematics for Systems Design (MMSD). It is led by Ichiro Hasuo, with its principal sites in Tokyo, Japan and Waterloo, Canada.
This website at NII is supplementary to the official website at JST.
ERATO MMSD started on October 1, 2016.
Job Description
Applications are invited for 10+ senior researchers and postdocs for the project, from the fields including (but not restricted to): formal methods, programming languages, software science, software engineering, control theory, machine learning, (numerical) optimization, user interface, mathematical logic and category theory (see below for further details on technical qualifications). We also invite applications for research assistants and research interns.
You will belong to Group 0, 1 or 3 of the project and and work at the project site in central Tokyo. The site is next to National Institute of Informatics (NII), an institute that is dedicated to IT research and hosts 70+ faculty members and another 50+ researchers. The institute (together with the ERATO MMSD project) will provide you with a highly creative environment suited for conducting globally competitive research.
You should be (self-)motivated, dedicated, and able to work both independently and collaboratively. The project is of an interdisciplinary nature: breadth of interests beyond your own field and the willingness and ability to move back-and-forth between theory and practice are mandatory. Strong communication skills in oral/written English are required, too. The positions are initially until the end of a fiscal year (Mar 31), with the possibility of extension (maximum until the project ends in March 2022).
Senior Researchers
You will play a leading role in the research activities of the group (G0, G1 or G3), as well as in initiating new inter-group collaborations. You need a PhD degree, a proven global publication record, and a record of research leadership. The annual gross salary is based on your qualifications; it starts at approximately JPY 6,000,000 (and goes potentially much higher). It is possible that you will be granted an academic title (like Project Assistant/Associate Professor).
Postdocs
You will pursue your research agenda, in line with the project's goal of applying formal methods to manufacturing. You are strongly encouraged to spend at least 30% of your time for research beyond your core topic (e.g. working with people from different disciplines, and extending your realm in the theory-application spectrum). You need a PhD degree (or be close to completion) and a proven publication record. Experience of actively collaborating for publication is highly desirable. The annual gross salary is based on your qualifications; it starts at approximately JPY 4,250,000.
Research Assistants (PhD Students)
PhD degrees are available through your supervisor's affiliation. Although it's been the norm for PhD students in Japan to self-fund their study, there are some funding schemes for talented students. Among them are the ERATO research assistant positions, from which you will get approximately JPY 2,400,000 annually. You are encouraged to contact your prospective supervisor chosen from our member list.
Research Interns
We accept student interns. You are encouraged to contact your prospective supervisor chosen from our member list.
Desired Technical Qualifications
Our project is big and diverse; there are many different ways in which you can contribute to the project's goal (extending the realm of formal methods from software to cyber-physical systems and manufacturing). Your research activities will be aligned with the mission of one of our four groups. Examples of technical qualifications of successful candidates--besides the non-technical requirements described above--include (but are not restricted to) the following.
Group 0: Metatheoretical Integration
Mathematical logic (e.g. proof theory, model theory, modal logic, etc.) with experience or eagerness to apply theory to real-world problems.
Category theory (especially its use in computer science via coalgebras and other disciplines) with experience or eagerness to apply theory to real-world problems.
Experience in verification algorithms, tools and real-world applications is not mandatory; but eagerness to work on them is mandatory. As a guideline we expect you to strive for publications in venues like CAV, TACAS, FM, HSCC, etc. (where a paper would have a "case study"), potentially through collaboration with others.
Group 1: Heterogeneous Formal Methods
- Automata-theoretic techniques, especially with quantities (probabilities, time, weights, etc.).
- Programming language theory, especially its application to program verification (program logics, program model checking, abstract interpretation, type systems).
- Control theory with experience or eagerness to deal with hybrid dynamics.
- Hybrid systems, including reachability analisys, controller synthesis, falsification and specification mining.
- Continuous or discrete optimization with eagerness to work with other disciplines to solve real-world problems.
Group 3: Formal Methods and Intelligence
- Formal engineering methods that make effective use of formal specifications, abstraction/refinement, verification techniques, and so on.
- Software engineering and systems engineering, especially model-based approaches to support design and assurance (simulation, model-based testing, assurance cases, etc.).
- User interface and human-computer interaction for computer-aided XXX, where XXX can be verification, decision making for complex problems, etc.
- Machine learning and/or artificial intelligence, with specific examples including MSR (mining software repository) approaches and others.
For Group 3, eager and open minds are particularly valued in pursuit of integration of diverse areas such as the above. Experiences in interdisciplinary integration is (not mandatory but) highly welcome.
Applications and Inquiries
Applications should be sent to application_eratommsd [at] group-mmm.org, with the subject "ERATO Job 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.
Starting dates are flexible. The 10+ positions will remain open until filled. The project ends in March 2022; several positions are still open as of April 2017.
Inquiries should also be sent to application_eratommsd [at] group-mmm.org, with the subject "ERATO Job Inquiry."
Living and Working 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 far below the standard in US).
Prices
Rumors have it that Tokyo is a prohibitively expensive place to live in. It is hardly the case in reality, especially if you are fine with adjusting a little to a local lifestyle. 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 most locals rarely have either :) : JPY 30,000
- A pint of beer: JPY 700
Apartments
You can easily find an apartment using the following websites: www.sabbaticalhomes.com, www.sakura-house.com/en, gaijinpot.com, and others.
Language
Yes it is true that most locals don't speak English. Being in Tokyo is a big advantage, though: it's a huge city with at least a certain level of cosmopolitan atmosphere; it won't be hard to find friends from overseas as well; and with the next 2020 Olympic games planned in Tokyo, the city is getting better prepared to host people coming from abroad. Besides, the project takes it very seriously to nurture an international working environment: its working language is English; all the staff (including the admin support) will speak English; and most of the core people of the project (Director, Group Leaders) have experience of working overseas.