小島健介

J-GLOBALへ         更新日: 16/12/22 22:55
 
アバター
研究者氏名
小島健介
所属
京都大学
職名
研究員
学位
博士(情報学)(京都大学)

プロフィール

最近はプログラム検証の研究をしています。
現在の主なトピックは GPGPU プログラムの検証と不変条件の生成です。
論理学・型理論にも興味があります。

研究分野

 
 

論文

 
SIMTのためのHoare論理のCoqを用いた形式化と並列prefix-sumアルゴリズムの検証
奥村 健太郎, 小島 健介, 五十嵐 淳
第18回プログラミングおよびプログラミング言語ワークショップ論文集      2016年3月   [査読有り]
Kensuke Kojima, Akifumi Imanishi and Atsushi Igarahi
to appear in the postproceedings of VSTTE 2016      2016年   [査読有り]
Kensuke Kojima, Minoru Kinoshita, and Kohei Suenaga
to appear in the proceedings of SAS 2016      2016年   [査読有り]
Kensuke Kojima and Atsushi Igarahi
submitted      2014年
Kensuke Kojima and Atsushi Igarashi
Information and Computation   209(12) 1491-1503   2011年12月   [査読有り]

講演・口頭発表等

 
Formal Verification of the Correctness of CUDA Programs Using Hoare Logic
小島健介, 五十嵐淳
International Symbosium on Post Petascale System Software   2014年12月2日   
Generic GluonJ に向けて
小島健介, 五十嵐淳
PPL 2014   2014年3月5日   
SIMT プログラムのためのホーア論理
小島健介, 五十嵐淳
PPL 2013   2013年3月4日   
Birelational Kripke semantics for an intuitionistic LTL
Kensuke Kojima
Topology, algebra and categories in logic (TACL) 2009   2009年7月   
On Constructive Linear-Time Temporal Logic
Kensuke Kojima
Intuitionistic modal logic and applications (IMLA) '08   2008年6月