酒井政裕

J-GLOBALへ         更新日: 18/11/06 19:17
 
アバター
研究者氏名
酒井政裕
所属
Preferred Networks, Inc.
職名
Engineer
学位
修士(政策・メディア)(慶應義塾大学)
Twitter ID
masahiro_sakai

プロフィール

2007年3月慶應義塾大学政策・メディア研究科修士課程修了.2007年4月より,(株)東芝 研究開発センター システム技術ラボラトリー.ソフトウェアの設計・検証技術の研究に従事.訳書(共訳)に『抽象によるソフトウェア設計-Alloyではじめる形式手法-』『型システム入門-プログラミング言語と型の理論-』.

Blog: msakai.jp/d/
Twitter: http://twitter.com/masahiro_sakai
CiteULike: http://www.citeulike.org/users/msakai
Google+: https://plus.google.com/+MasahiroSakai/
Facebook: https://www.facebook.com/masahiro.sakai

研究分野

 
 

経歴

 
2017年5月
 - 
現在
Preferred Networks, Inc. Engineer
 
2007年4月
 - 
2017年4月
株式会社東芝 研究開発センター システム技術ラボラトリー
 
2005年4月
 - 
2007年3月
慶應義塾大学大学院 政策・メディア研究科 修士課程
 
2001年4月
 - 
2005年3月
慶應義塾大学 総合政策学部
 

受賞

 
2017年4月
株式会社東芝 研究開発センター 業績賞優秀賞
 
2015年
日本ソフトウェア科学会 日本ソフトウェア科学会第19回研究論文賞
受賞者: 今井健男, 酒井政裕, 萩谷昌己
 
2014年7月
株式会社東芝 コミュニティ・ソリューション社 知的財産活動奨励賞
 

論文

 
Mitsuru Kusumoto, Keisuke Yahata, Masahiro Sakai
   2018年11月
The problem-solving in automated theorem proving (ATP) can be interpreted as a search problem where the prover constructs a proof tree step by step. In this paper, we propose a deep reinforcement learning algorithm for proof search in intuitionist...
ICFP 2016 参加報告
酒井政裕
コンピュータソフトウェア   34(1) 62-66   2017年2月
今井 健男, 酒井 政裕, 萩谷 昌巳
コンピュータソフトウェア   32(4) 161-175   2015年11月   [査読有り]
我々は以前,制約ソルバを用いて,自動生成した述語の組み合せからなるプログラムの事前条件で最弱なもの(準最弱事前条件)を推定する手法を提案した.これには minimal unsatisfiable core (MUC) の列挙を利用していたが,計算コストが高いことが主な課題であった. MUCの列挙は minimal correction subset (MCS) の列挙を介して実現できるが,MUCの列挙が高コストである要因の1つは,このMCS列挙の高コスト性にある.

我々は本手法を通じて得...
地域活性化のためのスマートフォンアプリを用いた実店舗および商品の推薦
酒井 政裕, 高 明淑, 西沢 孝浩, 阿部 真美子
第 14 回情報科学技術フォーラム   2 303-306   2015年9月
川崎市と東芝は,コミュニティ内の商業施設全体を活性化すると共に,消費者であるコミュニティ住民の生活を豊かで楽しくすることを目指し,川崎駅周辺の複数商業施設をクラウド上で仮想的に連携させ,ユーザの嗜好に応じた情報をスマートフォンアプリ上に配信し,購買行動などの検証を行う実証実験「川崎グランシティモールTM」を行った.本稿では,当実証実験の一環として行った,利用者のアンケート回答および店舗・商品に対する評価履歴の情報に基づいた実店舗および商品の情報の推薦について,用いた推薦アルゴリズム,得られ...
酒井政裕, 今井健男
コンピュータソフトウェア   32(1) 103-119   2015年2月   [査読有り]
SAT問題は,命題論理式の充足可能性問題,すなわち命題変数を含む論理式に対し,その論理式を真にするような命題変数への値の割り当てが存在するかを決定する問題である.SATは古典的なNP完全問題であり,計算量的には難しい問題であるものの,近年のアルゴリズムの改良とハードウェアの進化によって著しい高性能化が実現された結果として,様々な分野への応用が行われている.本稿ではSATにまつわる研究で現在活発な領域として,関連する問題クラスへの応用やそれにまつわる研究分野との間の交流について,調査し,紹介する.

Misc

 
PLC言語向け モデルベーステスト技術
丸地 康平,進 博正,酒井 政裕
東芝レビュー   67(3) 38-38   2012年3月
C言語プログラム検証フレームワーク
酒井政裕, 今井健男, 片岡欣夫
東芝レビュー   64(3) 41-41   2009年3月
Haskellによる関数プログラミング入門
酒井政裕
日経ソフトウェア   62-69   2006年6月

書籍等出版物

 
抽象によるソフトウェア設計
Daniel Jackson, 中島 震, 今井 健男, 酒井 政裕, 遠藤 侑介, 片岡欣夫 (担当:共訳)
オーム社   2011年7月   ISBN:978-4-274-06858-4
D. Jackson, "Software Abstractions"の邦訳

講演・口頭発表等

 
A Decision Table Analyzer for Detecting Variability in Source Code
Masahiro Sakai, Takeo Imai, Mikito Iwamasa, Takeshi Nagaoka and Mari Inoki
Fourth Workshop on Formal Methods and Analysis in Software Product Line Engineering (FMSPLE 2013)   2013年8月27日   
説明基盤:組み込みシステムの要求仕様を形式的に分析・検証する一手法
今井健男,岩政幹人,遠藤侑介,酒井政裕,鳥居健太郎
第19回 ソフトウェア工学の基礎ワークショップ FOSE 2012   2012年12月   
本発表では、組み込みシステムの要求仕様を分析するための、半形式的なドキュメント「説明基盤」の概念を新たに導入する。その上で、日本語の要求仕様から自然言語処理技術を介して説明基盤を求め、形式手法の技術を使って解析することにより、元の要求仕様の妥当性を検証する方法論、および、その機械的支援手法を提案する。今回は解析に仕様記述言語Alloyとその解析器Alloy Analyzerを援用し、専用のイディオムも併せて提案する。
仮想的なタグを用いた共用体入りプログラムの事前条件推定
今井 健男, 酒井 政裕, 遠藤 侑介, 萩谷 昌己
In 第14回プログラミングおよびプログラミング言語ワークショップ   2012年3月   日本ソフトウェア科学会 プログラミング論研究会
本発表では、共用体を用いた C 言語プログラムの検証方法を提案する。本手法では、共用体変数が直和型を持つと読み替える。具体的には、代入時、代入されたフィールドと同じ型タグを付加的に記憶し、また、タグと異なるフィールドからの読み出しで例外を発生するようにプログラムを読み替える。その上で、我々の先行研究に基づき、プログラムテキストから生成した述語の組み合わせで最も弱い事前条件(準最弱事前条件)を有界モデル検査器を使って求めることで、共用体を用いたプログラムが安全に利用される条件を推定する。我々...
遠藤侑介,酒井政裕,今井健男,岩政幹人
ソフトウェアエンジニアリングシンポジウム2011   2011年9月   
運用中のソフトウェアでは,運用時の修正や派生開発によって,設計仕様書に書 かれた各機能がどのモジュールで実現されているか不明確になっていることが 散見される.本発表ではテストカバレッジを介して設計仕様書とモジュール間の 対応を復元するツール eacov を解説する.我々は,設計仕様書とテストケースの 対応が比較的維持されているという前提に立ち,テストケースを「文書」,その テストで実行された箇所の集合を「単語の集合」とみなして,自然言語処理に用 いられる特徴語抽出手法である TF-IDF ...

Works

 
コンピュータソフト   

特許

 
遠藤 侑介, 進 博正, 岩政 幹人, 丸地 康平, 酒井 政裕
丸地 康平, 酒井 政裕, 進 博正, 吉澤 晋, 酒井 宏隆, 新田 能之, 吉田 順陽, 梅村 憲弘, 服部 可奈子