Author: Ichiro Hasuo

We invite applications for postdoc and senior researchers. The candidates will pursue collaboration with Bart Jacobs (Nijmegen), Joost-Pieter Katoen (Aachen), and Sam Staton (Oxford). The positions are for 4.5 years max.

• [Abstract and Concrete Automated Verification]
  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.
• [Mathematical Logic for Software, Systems, and Society]
  We look for formal verification specialists (theorem proving or model checking) with aspiration to take up real-world problems.
• [Open Call]
  One or two researchers without specified topics. Can be senior or junior.

Symposium information: https://group-mmm.org/eratommsd/ja/2024symposium/

Most talks are in Japanese… but join us for poster presentations and discussions! Registration deadline: Fri 7 June.

A paper by Mayuko Kori, Ichiro Hasuo and others was awarded as Distinguished Paper Award of 35th International Conference on Computer Aided Verification. 

Authors
Mayuko Kori (National Institute of Informatics & SOKENDAI)
Flavio Ascari (University of Pisa) 
Filippo Bonchi (University of Pisa) 
Roberto Bruni (University of Pisa) 
Roberta Gori (University of Pisa) 
Ichiro Hasuo (National Institute of Informatics & SOKENDAI)

Awarded Paper Title
Exploiting Adjoints in Property Directed Reachability Analysis

Mayuko Kori is a PhD student at SOKENDAI/NII, a JSPS Research Fellow (DC), and a research assistant at ERATO MMSD (Group 0).

Three papers (co)-authored by ERATO MMSD researchers accepted for presentation at CAV 2023 – 35th International Conference on Computer Aided Verification.

• Compositional Probabilistic Model Checking with String Diagrams of MDPs. Kazuki Watanabe, Clovis Eberhart, Kazuyuki Asada, Ichiro Hasuo
• Online Causation Monitoring of Signal Temporal Logic. Zhenya Zhang, Jie An, Paolo Arcaini, Ichiro Hasuo
• Exploiting Adjoints in Property Directed Reachability Analysis. Mayuko Kori, Flavio Ascari, Filippo Bonchi, Roberto Bruni, Roberta Gori, Ichiro Hasuo

The CAV Conference is a top international venue on computer-aided formal analysis methods for hardware and software systems. CAV 2023 will take place in Paris, Frande, in July 2023.

A few positions with us are now open:

• Scientific Programmer (Towards a Research-Oriented Startup, Oct 2022)
• PostDoc Researcher (Category Theory and Practical Model Checking Algorithms, Oct 2022)
• PostDoc Researcher (Theorem Proving for Automated Driving, Oct 2022)

Besides, there is a post-doc opportunity open in Kyoto, in Atsushi Igarashi’s group (we work closely with them):

• PostDoc Researcher (Programming abstraction for security, Kyoto U)

A news release from NII and JST:

The research team led by HASUO Ichiro at the National Institute of Informatics (NII, Japan) developed a methodology to provide strong mathematical safety guarantees to automated driving vehicles, together with its underlying theory on formal logic. This research was conducted under the ERATO MMSD project funded by the Japan Science and Technology Agency (JST, Japan).

Building on the existing methodology called “Responsibility-Sensitive Safety (RSS)” for mathematical proofs of automated driving safety, the research established its extension called “Goal-Aware RSS (GA-RSS)” that expands RSS’s application domain to a variety of real-world driving scenarios. Specifically, the techniques in GA-RSS derived from theoretical results in formal logic enable one to provide mathematical safety proofs to more complex driving scenarios than before, especially those which require achievement of certain goals such as an emergency stop.

The outcome of this research was published in IEEE Transactions on Intelligent Vehicles, a top journal on automated driving on July 5, 2022 (US Eastern Time).

Links

• News release
• Paper (IEEE)
• Paper (arXiv preprint version, open access)
• Introduction video on YouTube

The following positions are currently open.

• Scientific programmer
• PostDoc researcher in formal verification extended with optimization metaheuristics

Three papers (co)-authored by ERATO MMSD researchers accepted for presentation at ETAPS 2020 – European Joint Conferences on Theory and Practice of Software.

• Juraj Kolčák, Jérémy Dubut, Ichiro Hasuo, Shin-Ya Katsumata, David Sprunger and Akihisa Yamada. Relational Differential Dynamic Logic. 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020) 
• Takamasa Okudono and Andy King. Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic. 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020)
• Satoshi Kura. Graded algebraic theories. 23rd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2020)

The European Joint Conferences on Theory and Practice of Software (ETAPS) is the primary European forum for academic and industrial researchers working on topics relating to Software Science. ETAPS, established in 1998, is a confederation of four main annual conferences, ESOP, FASE, FOSSACS and TACAS, accompanied by satellite workshops and other events. ETAPS 2020 conference was planned in Dublin, Ireland, in April 2020 (postponed due to COVID-19).

Dr. Xiaoyi Zhang, Dr. Paolo Arcaini and Dr. Fuyuki Ishikawa have been awarded the best paper award at ICECCS 2019 — the 24th International Conference on Engineering of Complex Computer Systems.

Xiao-Yi Zhang, Paolo Arcaini, Fuyuki Ishikawa:
Assessing the Relation Between Hazards and Variability in Automotive Systems. ICECCS 2019: 190-199. [ieee]

The three authors are members of ERATO MMSD Project (Group 3, led by Fuyuki Ishikawa).

ICECCS is one of the top international conferences in the field of formal methods (CORE rank A). This is the second best paper award in a row at ICECCS from ERATO MMSD, following the last year.

Two papers authored by ERATO MMSD researchers accepted for presentation at ITSC 2019 – the 22nd International Conference on Intelligent Transportation Systems.

Chao Huang, Boyuan Li, Masako Kishida. Model predictive approach to integrated path planning and tracking for autonomous vehicles. IEEE Intelligent Transportation Systems Conference (ITSC 2019), 2019
[doi | arxiv]

Sasinee Pruekprasert, Xiaoyi Zhang, Jérémy Dubut, Chao Huang. Decision Making for Autonomous Vehicles at Unsignalized Intersection in Presence of Malicious Vehicles. IEEE Intelligent Transportation Systems Conference (ITSC 2019), 2019
[doi | arxiv]

The ITSC Conference is a major international venue on intelligent transportation systems, including automated driving. ITSC 2019 took place in Auckland, New Zealand, in October 2019.