今井 健男

J-GLOBALへ         更新日: 17/04/23 20:52
 
アバター
研究者氏名
今井 健男
eメール
takeo.imaitoshiba.co.jp
所属
(株)東芝
部署
研究開発センター システム技術ラボラトリー
職名
研究主務
学位
修士(理学)(東京大学)
その他の所属
東京大学大学院 情報理工学系研究科

研究分野

 
 

受賞

 
2015年9月
日本ソフトウェア科学会 第19回研究論文賞
 
2011年11月
第18回 ソフトウェア工学の基礎ワークショップ 貢献賞
 

論文

 
酒井 政裕, 今井 健男
コンピュータ ソフトウェア   32(1) 1_103-1_119   2015年
SAT問題は,命題論理式の充足可能性問題,すなわち命題変数を含む論理式に対し,その論理式を真にするような命題変数への値の割り当てが存在するかを決定する問題である.SATは古典的なNP完全問題であり,計算量的には難しい問題であるものの,近年のアルゴリズムの改良とハードウェアの進化によって著しい高性能化が実現された結果として,様々な分野への応用が行われている.本稿ではSATにまつわる研究で現在活発な領域として,関連する問題クラスへの応用やそれにまつわる研究分野との間の交流について,調査し,紹介する.
今井 健男, 酒井 政裕, 萩谷 昌己
コンピュータ ソフトウェア   30(2) 2_207-2_226   2013年
本稿では,プログラムの事前条件推定を行う新たな手法を提案する.本手法では,プログラムのテキストから生成した述語の集合とプログラムに相当する論理式,および事後条件の否定の連言を作り,そのMinimal Unsatisfiable Core(MUC)から事前条件を求める.MUCは一般的に複数存在するが,本手法ではまずMUCを列挙し,その中から事前条件として適格で,かつ最も弱い条件を選択する.こうして得られる事前条件は理想的な最弱条件ではないが,与えられた述語群の組み合わせの中で最も弱いという点...
今井 健男, 山本 泰宇, 遠藤 敏夫, 田浦 健次朗, 米澤 明憲
情報処理学会論文誌. プログラミング   40(1) 42-56   1999年2月   [査読有り]
我々は, C++に分散オブジェクトと分散ごみ集め(分散GC)機構を導入した, 分散記憶型並列計算機向け拡張言語DisCを開発する. 我々はまず, 分散オブジェクトをC/C++上で扱うためのライブラリ(GCライブラリ)を開発する. これは, オブジェクトがどのプロセッサ上にあるのかの判定, あるいは遠隔参照の明示的な作成等, 分散オブジェクトの基礎的な機能を実現する. そしてこのライブラリに対し, 動的にゴミとなった分散オブジェクトを回収する分散ごみ集めの機能を導入する. このごみ集め機構は...

書籍等出版物

 
Benjamin C. Pierce (担当:共訳)
オーム社   2013年3月   ISBN:4274069117
Daniel Jackson (担当:共訳)
オーム社   2011年7月   ISBN:4274068587

講演・口頭発表等

 
高速なMCS列挙を利用した準最弱事前条件推定の改良
今井 健男, 酒井 政裕, 萩谷 昌己
第21回ソフトウェア工学の基礎ワークショップ (FOSE 2014)   2014年12月12日   
論理制約ソルバを用いたプログラムの事前条件推定 [招待有り]
今井 健男
平成24年度情報処理学会関西支部大会   2012年9月21日   
遠藤 侑介, 酒井 政裕, 今井 健男, 岩政 幹人, 福元 康文, 一條 泰男
ソフトウェアエンジニアリングシンポジウム2012論文集   2012年8月21日   
仮想的なタグを用いた共用体入りプログラムの事前条件推定
今井 健男, 酒井 政裕, 遠藤 侑介, 萩谷 昌己
第14回プログラミングおよびプログラミング言語ワークショップ(PPL2012)   2012年3月8日   
Minimal Unsatisfiable Core列挙によるプログラムの準最弱な事前条件推定
今井 健男, 酒井 政裕, 萩谷 昌己
ソフトウェア工学の基礎ワークショップ   2011年11月