皆様、

千葉工業大学の安部達也です。

筑波大学の海野広志さん（http://www.cs.tsukuba.ac.jp/~uhiro/%EF%BC%89%E3%81%AB%E6%9C%80%E6%96%B0%E3%8... プログラム検証・合成についてお話しいただく機会を得ることができました。 つきましては、公開の講演会という形式で開催することにしましたので、ぜひ ご参加ください。

日時：2020年12月18日（金）15:00--16:00 場所：オンライン会場 参加費：無料

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

参加方法：https://stair-st.connpass.com/ で参加登録をしてください。 参加登録をした人だけがアクセスできるウェブページに会場 URL を記載しています。

問合せ先：abe.tatsuya@it-chiba.ac.jp