【終了】第1回ステアラボソフトウェア技術セミナー 海野広志 先生「制約解消によるプログラム検証・合成」 The 1st STAIR Lab ST Seminar: Dr. Hiroshi Unno, "Program Verification and Synthesis by Constraint Solving"

We have been regularly organizing STAIR Lab AI seminars, which mainly focus on artificial intelligence topics including machine learning, natural language processing, and so on. In addition to them, we decided to hold STAIR Lab ST seminars online, which focus on research topics in software technology.

千葉工業大学 人工知能・ソフトウェア技術研究センター (ステアラボ) では、従来機械学習や自然言語処理等の人工知能に関するセミナー (ステアラボ人工知能セミナー) を開催して参りましたが、この度、ソフトウェア技術研究に関するセミナーもオンライン形式で開催することに致しました。

Everyone can participate for free. Theoretically, there is no limit on the number of participants because they are held online.
We are looking forward to your participation.

どなたでも無料でご参加いただけます。オンライン形式のため特に定員数は設けておりませんので皆様奮ってご参加ください。

【日時】
2020年12月18日 (金) 15:00-16:00

Date:
Dec. 18, 2020 (Fri.) 15:00 – 16:00

【講演形態】
オンライン

Venue:
Online

【講演者】
筑波大学 システム情報系 准教授 海野 広志 先生
http://www.cs.tsukuba.ac.jp/~uhiro/

Speaker:
Hiroshi Unno, Graduate School of Systems and Information Engineering, University of Tsukuba
http://www.cs.tsukuba.ac.jp/~uhiro/

【講演タイトル】
制約解消によるプログラム検証・合成

Title:
Program Verification and Synthesis by Constraint Solving

【講演概要】
SMTソルバの発展により、整数、実数、リスト、配列といった様々なデータ上の論理制約を高速に解くことが可能となり、プログラム検証への応用が加速した。しかし、SMTソルバは関数上の論理制約を解くことができないため、ループや再帰関数を含むプログラムの検証やプログラム合成に直接応用することはできない。本講演では、最近盛んに研究されている関数上の制約解消問題であるSyGuS、CHCおよびそれらの一般化とプログラム検証・合成への応用について説明した後、関数上の制約解消法の一つである反例駆動帰納的合成法（CEGIS）について紹介する。CEGISはデータ駆動であるため、機械学習と相性がよい。本講演ではCEGISと機械学習の融合についても論じる。

The details are written in Japanese and the talk will be given in Japanese.