木村大輔講師の共著論文が日本ソフトウェア科学会 研究論文賞 (Best Research Paper Award) を受賞しました．
日本ソフトウェア科学会 第26回研究論文賞

著者：Koji Nakazawa, Makoto Tatsuta, Daisuke Kimura, Mitsuru Yamamura
論文タイトル：Spatial Factorization in Cyclic-Proof System for Separation Logic
掲載誌：コンピュータソフトウェア, Vol. 37, No. 1 (2020)

内容紹介
書かれたプログラムが仕様通りであることを数学的に証明する手法を「プログラム検証」とよびます． 分離論理 (Separation Logic) はメモリの状態を簡潔な記述で書くことができる論理体系で， プログラムの仕様を形式的に記述するために用いられます． この論文では分離論理の循環証明体系 (Cyclic-proof system) における証明探索の新たなアルゴリズムを提案し， その正当性を数学的に証明し，アルゴリズムの実装と実験によって有効性を示しました．

今回の研究論文賞は学会誌「コンピュータソフトウェア」に2020年に掲載された全論文の中から とくに優れた研究論文2件に対して与えられられたものです．