ERATO MMSD – ERATO Metamathematics for Systems Design Project

博士研究員・特任教員募集

数名の研究員を募集しています．ぜひご検討ください．

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.

ERATO MMSD 成果報告会を開催しました

ERATO MMSD 成果報告会を 2024年6月19日（水）に開催し，109名の方々にご参加いただきました．みなさま本当にありがとうございました．

当日の講演動画はこちらでご覧いただけます．

ERATO MMSD 成果報告会開催

6月19日（水）に開催します．詳細はこちら：
https://group-mmm.org/eratommsd/ja/2024symposium/

関連する研究分野の方のみならず，産業界のみなさまや，研究プロジェクトの運営・支援・制度設計に関わる方にも，ご参加いただきたく思っております．

参加登録は2024年6月7日（金）までにお願いいたします．

Distinguished paper award 受賞

郡茉友子，蓮尾一郎らの論文が 35th International Conference on Computer Aided Verification にて “Distinguished paper award” を受賞

受賞者
Mayuko Kori (国立情報学研究所・総合研究大学院大学)
Flavio Ascari (University of Pisa)
Filippo Bonchi (University of Pisa)
Roberto Bruni (University of Pisa)
Roberta Gori (University of Pisa) Ichiro Hasuo (国立情報学研究所)

受賞論文タイトル
Exploiting Adjoints in Property Directed Reachability Analysis

郡茉友子はERATO MMSD プロジェクトのリサーチアシスタント（グループ０）です。彼女は総研大情報学専攻の博士課程に在学中であり，日本学術振興会特別研究員（DC）でもあります．

3報の論文が CAV 2023 に採択

ERATO MMSD プロジェクトの研究者が著者となる3報の論文が， 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

International Conference on Computer-Aided Verification (CAV) は形式検証分野のトップ国際会議です．CAV 2023 は2023年7月にパリで開催されます．

自動運転車の安全性の数学的証明についての雑誌記事公開

自動運転車の安全性の数学的証明について，岩波書店科学 2023年3月号に掲載された解説記事を公開しています．数理論理学の（超高速）入門も兼ねています．

蓮尾一郎「自動運転車の安全性の数学的証明――論理学の社会応用の一例として」科学 2023年3月号，岩波書店

採用情報

以下のポジションで研究員・プログラマーを募集しています．ぜひ国内からの応募もご検討ください．

関連して，協力して研究を行っている京都大学五十嵐・末永研究室でも，次の求人があります．

博士研究員募集（IoTセキュリティのためのプログラミング言語理論，京都大学）

自動運転車の安全性に数学的証明を与える新手法を開発
～論理的安全ルールの効率的導出により自動運転の社会受容を加速～

以下の論文の成果を，NII および JST からニュースリリースしました．

情報・システム研究機構国立情報学研究所（ＮＩＩ、所長：喜連川優、東京都千代田区）のアーキテクチャ科学研究系教授蓮尾一郎らの研究チームは、科学技術振興機構（ＪＳＴ、理事長：橋本和仁、東京都千代田区）の戦略的創造研究推進事業ＥＲＡＴＯ蓮尾メタ数理システムデザインプロジェクト（ＥＲＡＴＯＭＭＳＤ、研究総括：ＮＩＩアーキテクチャ科学研究系教授蓮尾一郎）のもと、自動車の自動運転システムの安全性に強い数学的保証を与える技術とその基礎理論を開発しました。

本研究では、自動運転安全性の数学的証明のための既存の方法論「ＲＳＳ（責任感知型安全論、responsibility-sensitive safety）」に注目し、その応用範囲を大きく拡大し実世界へ本格展開できるよう拡張した手法「ＧＡ－ＲＳＳ（goal-aware RSS）」を確立しました。形式論理学の知見を用いた今回の拡張によって、非常停止などの目標達成を求める複雑な運転シナリオに対しても、安全性の数学的証明が可能になります。

本研究成果は、２０２２年７月５日（米国東部時間）に、「IEEE Transactions on Intelligent Vehicles」のオンライン版で公開されました。

リンク

採用情報

以下のポジションで研究員・プログラマーを募集しています．ぜひ国内からの応募もご検討ください．

自動運転における重大な問題をシミュレーションで検出する技術を開発
～問題が発生するかを探り、起こりうる問題だけを効率的に自動探索～

以下の論文の成果を，NII および JST からニュースリリースしました．

情報・システム研究機構国立情報学研究所（NIIエヌアイアイ、所長：喜連川優、東京都千代田区）のアーキテクチャ科学研究系准教授石川いしかわ冬樹ふゆきらの研究チームは、科学技術振興機構（JSTジェイエスティー、理事長：濵口道成、東京都千代田区）の戦略的創造研究推進事業 ERATOエラトー蓮尾メタ数理システムデザインプロジェクト（ERATO MMSD、研究総括：NIIアーキテクチャ科学研究系准教授蓮尾一郎）のもと、自動運転システムのシミュレーションにおいて、急加速や急ハンドルが起きているなど事故につながるような複合的で重大な問題が発生するシミュレーションシナリオを効率よく自動で見つける技術を開発しました。

本手法では、シミュレーションの試行を繰り返す中で、追い越しや右折などのシナリオごとに起こりえない問題を見つけて不要なシミュレーション試行を除外することで、重大な問題が起きるような本当に重要なシナリオ、例えばあまりにも強い加速と急ハンドルが同時に発生するなどの状況を効率的に見つけ出すことができます。

　本研究成果は、ソフトウェア工学における自動化についてのフラッグシップ国際会議ASE 2021で2021年11月16日（オーストラリア時間）に発表されました。

NIIからのニュースリリース