研究テーマ

自動プログラム検証に有用な論理式の自動生成手法

研究者名 末永 幸平 研究者所属 京都大学 大学院情報学研究科
キーワード プログラム検証、不変条件、システムの安全性担保，物理情報システム，IoT

---

研究内容

A：どんな諸分野・企業の、どんな問題や現象をターゲットにしたか。

様々なシステムがソフトウェアの制御を受ける現代において，プログラムの安全性を担保することが多くの産業において重要な課題となっています．自動車産業や航空産業等の特に高度な安全性が求められる分野では，プログラムの安全性を数学的に証明する形式検証という技術が重要になっています．ただし，現在の形式検証技術ではプログラムが複雑になると検証が難しいという問題があります．

B：どんな数学・数理科学をどのように使ったか。

多項式の斉次性と呼ばれる概念を一般化して得られる一般化斉次多項式の性質や，Positivstellensatz と呼ばれる多項式を伴う不等式系に関する定理を，検証アルゴリズムにおいて用いています．

C：どんな成果が得られたか。(あるいは、どんな成果を目指しているか。)

一般化斉次多項式の性質を用いたアルゴリズムによって，従来のプログラム検証手法を最大で数十倍高速化することができました．また，Positivstellensatz から導かれる補題に基づいて，プログラム検証で頻繁に用いられる不等式系の充足不能性の証拠となる論理式を半正定値計画問題で生成する従来より強力な手法を開発しました．これらの成果を物理情報システムと呼ばれる，ソフトウェアで制御される物理システムの検証に適用することを目指しています．

D：どのようなきっかけでその諸分野・企業との連携が始まったか。

京都大学の新技術交流会での研究内容の紹介やこれらの技術に伴う発明の特許出願等をきっかけとして，複数の企業様からのコンタクトを受けております．

---