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

今回は筑波大学の海野広志先生に「制約解消によるプログラム検証・合成」というタイトルでご講演いただきます。

どなたでも無料でご参加いただけます。 参加申し込みをして頂くと具体的なアクセス情報が表示されます。オンライン形式のため特に定員数は設けておりませんので皆様奮ってご参加ください。

※ ただし、あまりに多数の申し込みを頂いた場合は参加登録を打ち切る等の対応をさせて頂く可能性もございますのでその際は何卒ご容赦下さい。
※ また、オンラインセミナー主催の経験がほとんど無いため、急遽開催できなくなったり、開催中に突然終了したりする事もあるかと存じますが、その際も何卒ご容赦下さい。

日時

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

講演形態

• オンライン: Cisco Webex Meetings を使用します。
  • 万が一不具合等により Cisco Webex Meetings が使用できない場合は、バックアップとして Microsoft Teams を使用します。
• アクセス方法は参加登録をして頂いた方にのみ公開されます。

講演者

筑波大学 システム情報系 准教授 海野 広志 先生

講演タイトル

制約解消によるプログラム検証・合成

講演概要

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