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

2020年12月18日(金)に第1回ステアラボソフトウェア技術セミナーをオンラインで開催しました。

今回は筑波大学の海野 広志先生をお招きして、「制約解消によるプログラム検証・合成」についてご講演いただきました。

講演ではまず、プログラム検証 (プログラムがある性質を満たしているか否かを数学的に厳密に証明すること) やプログラム合成 (ある性質を満たしているプログラムを自動的・機械的に生成すること) を数理論理学における制約解消問題に帰着する手法について、ご自身の研究成果を含め、研究の現状をご紹介頂きました。

また具体的に制約解消問題を解く手法として、従来の演繹的な手法 (SAT ソルバや SMT ソルバを用いる手法) と機械学習的な手法とを組み合わせる手法についてもご紹介頂きました。

We held the first STAIR Lab Software Technology Seminar on Dec. 18, 2020.
Dr. Hiroshi Unno, Graduate School of Systems and Information Engineering, University of Tsukuba, gave a talk titled “Program Verification and Synthesis by Constraint Solving”.

以下は講演スライドです。ぜひご覧ください!

The following is the talk slides (in Japanese). Please do have a look!

以下は講演動画です。ぜひご覧ください!

The following is the talk video (in Japanese). Please do have a look!