Masahiro Sakai

Profile Information

Affiliation: Engineer, Preferred Networks, Inc.

Degree: M.S. in Media and Governance(Keio University)

ORCID ID: https://orcid.org/0000-0003-4908-683X
J-GLOBAL ID: 201101069926322342
researchmap Member ID: B000001018

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

Blog: https://msakai.jp/d/
Twitter: http://twitter.com/masahiro_sakai
Facebook: https://www.facebook.com/masahiro.sakai

Research Interests

Research Areas

Research History

May, 2017 - Present

Engineer, Preferred Networks, Inc.
Apr, 2007 - Apr, 2017

System Engineering Laboratory, Corporate Research & Development Center, TOSHIBA Corp., Toshiba Corporation
Apr, 2005 - Mar, 2007

修士課程, 慶應義塾大学大学院政策・メディア研究科
Apr, 2001 - Mar, 2005

Faculty of Policy Management, Keio University

Awards

Apr, 2017

業績賞優秀賞, Research and Development Center, Toshiba Corporation
2015

日本ソフトウェア科学会第19回研究論文賞, Japan Society for Software Science and Technology

Takeo Imai, Masahiro Sakai, Masami Hagiya
Jul, 2014

知的財産活動奨励賞, Toshiba Corporation Community Solutions Company

Papers

Automated Theorem Proving in Intuitionistic Propositional Logic by Deep Reinforcement Learning

Mitsuru Kusumoto, Keisuke Yahata, Masahiro Sakai

Nov, 2018
Report on ICFP 2016

Masahiro Sakai

Computer Software, 34(1) 62-66, Feb, 2017
An Improvement of Quasi-weakest Precondition Inference using Fast MCS Enumeration

Takeo Imai, Masahiro Sakai, Masami Hagiya

Computer Software, 32(4) 161-175, Nov, 2015 Peer-reviewed
Brick-and-Mortar Shops/Goods Recommendation on Smart-Phone for Regional Promotion

Masahiro Sakai, Myungsook Ko, Takahiro Nishizawa, Mamiko Abe

Forum on Information Technology 2015, 2 303-306, Sep, 2015
Interplay between SAT and other Constraint Problems

Masahiro Sakai, Takeo Imai

Computer Software, 32(1) 103-119, Feb, 2015 Peer-reviewed
An improvement of quasi-weakest precondition inference using fast MCS enumeration

Takeo Imai, Masahiro Sakai, Masami Hagiya

21st Workshop on Foundation of Software Engineering (FOSE2014), 32(4) 93-102, Dec, 2014 Peer-reviewed
MC/DC-like Structural Coverage Criteria for Function Block Diagrams

Kohei Maruchi, Hiromasa Shin, Masahiro Sakai

2014 SEVENTH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE TESTING, VERIFICATION AND VALIDATION WORKSHOPS (ICSTW 2014), 253-259, 2014 Peer-reviewed
Specification Mining Technology for Automatically Inferring Software Specifications

Takeo Imai, Masahiro Sakai, Mikito Iwamasa

Toshiba Review, 68(8) 35-38, Aug, 2013
Minimal Unsatisfiable Core列挙によるプログラムの準最弱な事前条件推定

Takeo Imai, Masahiro Sakai, Masami Hagiya

コンピュータソフトウェア, 30(2) 207-226, May, 2013 Peer-reviewed
MTC: A New Test Coverage Criterion for Sequence Control Programs

Kohei Maruchi, Masahiro Sakai, Hiromasa Shin

情報処理学会第179回ソフトウェア工学研究発表会, 2013(17) 1-8, Mar, 2013
Supporting Technology for Modification of Existing Software Using Symbolic Execution

Masahiro Sakai, Mikito Iwamasa

Toshiba Review, 67(12) 35-38, Dec, 2012
Extracting a relation between test cases and modules by using important word analysis

Yusuke Endoh, Masahiro Sakai, Takeo Imai, Mikito Iwamasa, Fukumoto Yasufumi, Yasuo Ichijo

ソフトウェアエンジニアリングシンポジウム2012論文集, Aug, 2012 Peer-reviewed
Model-checking C programs against JML-like specification language

Masahiro Sakai, Kohei Maruchi, Takeo Imai

2012 19TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC), VOL 1, 174-183, 2012 Peer-reviewed
Trends and Future Goals of Specification Mining

Takeo Imai, Masahiro Sakai, Yusuke Endoh, Takashi Koiso, Mikito Iwamasa, Yoshio Kataoka

ウィンターワークショップ２０１２・イン・琵琶湖, 75-76, Jan, 2012
An Inference Method of Quasi-Weakest Preconditions by Minimal Unsatisfiable Core Enumeration

Takeo Imai, Masahiro Sakai, Masami Hagiya

18th Workshop on Foundation of Software Engineering (FOSE2011), 187-196, Nov, 2011 Peer-reviewed
Extracting Decision Tables from Programs using Symbolic Execution

Masahiro Sakai, Mikito Iwamasa, Yasuo Ichijo, Yasufumi Fukumoto

Proceedings of the 2011 IEICE Society Conference, Sep, 2011
CForge: Modular Verification Tool for C Programs Including Specification of Data Structures

Masahiro Sakai, Takeo Imai, Yoshio Kataoka

TOSHIBA Review, 64(8) 20-23, Aug, 2009
CForge: Bounded Model Checker for C Programs

Masahiro Sakai, Takeo Imai

Proceedings of JSSST Workshop on Programming and Programming Languages (PPL 2009), 118-132, Mar, 2009 Peer-reviewed
非正格関数の融合変換における始代数の存在について

Masahiro Sakai, Tatsuya Hagino

Proceedings of JSSST Workshop on Programming and Programming Languages (PPL 2008), 82-85, Mar, 2008 Peer-reviewed
Fusion Transformations Applicable to Non-Strict Functions

Masahiro Sakai

Jan, 2007

Misc.

チャーチ数あれこれ――テクニックから理論から応用まで

Masahiro Sakai

WEB+DB PRESS総集編［Vol.1～102］, 92-97, Apr, 2018 Lead author
PLC言語向けモデルベーステスト技術

Kohei Maruchi, Hiromasa Shin, Masahiro Sakai

TOSHIBA REVIEW, 67(3) 38-38, Mar, 2012
C言語プログラム検証フレームワーク

Masahiro Sakai, Takeo Imai, Yoshi Kataoka

TOSHIBA REVIEW, 64(3) 41-41, Mar, 2009
Haskellによる関数プログラミング入門

酒井政裕

日経ソフトウェア, 62-69, Jun, 2006

Books and Other Publications

型システム入門 : プログラミング言語と型の理論

Pierce, Benjamin C., Eijiro Sumii, Yusuke Endoh, Masahiro Sakai, Keigo Imai, Yusuke Kuroki, Yoshihiro Imai, Takafumi Saikawa, Takeo Imai (Role: Joint translator)

Ohmsha, Ltd., 2013 (ISBN: 9784274069116)
Software Abstractions (Japanese Translation)

Daniel Jackson, Shin Nakajima, Takeo Imai, Masahiro Sakai, Yusuke Endoh, Yoshio Kataoka (Role: Joint translator)

Ohmsha, Ltd., Jul, 2011 (ISBN: 9784274068584)

Presentations

BNN verification dataset for Max-SAT Evaluation 2020

Masahiro Sakai

NII Shonan Meeting (No.180) on “The Art of SAT”, Oct 3, 2023 Invited
Tree-width Prediction using Graph Neural Network

Yuta Nakano, Masahiro Sakai, Kohji Liu

基盤(S) 離散構造処理系プロジェクト 2019年度秋のワークショップ, Nov 5, 2019
A Decision Table Analyzer for Detecting Variability in Source Code

Masahiro Sakai, Takeo Imai, Mikito Iwamasa, Takeshi Nagaoka, Mari Inoki

Fourth Workshop on Formal Methods and Analysis in Software Product Line Engineering (FMSPLE 2013), Aug 27, 2013
説明基盤：組み込みシステムの要求仕様を形式的に分析・検証する一手法

Takeo Imai, Mikito Iwamasa, Yusuke Endoh, Masahiro Sakai, Kentaro Torii

第19回ソフトウェア工学の基礎ワークショップ FOSE 2012, Dec, 2012
仮想的なタグを用いた共用体入りプログラムの事前条件推定

Takeo Imai, Masahiro Sakai, Yusuke Endoh, Masami Hagiya

The 14th JSSST Workshop on Programming and Programming Languages, Mar, 2012
Eacov: extracting a relation between specifications and programs by using important word analysis

Yusuke Endoh, Masahiro Sakai, Takeo Imai, Mikito Iwamasa

IPSJ/SIGSE Software Engineering Symposium (SES2011), Sep, 2011

Professional Memberships

JAPAN SOCIETY FOR SOFTWARE SCIENCE AND TECHNOLOGY

Works

Ruby-GNOME2

Software
Ruby-GNOME2

Software

Industrial Property Rights

特開2016-062511 情報処理装置、情報処理システム、情報処理方法及びプログラム

Masahiro Sakai, Myungsook Ko, Eiichi Sunagawa, Takahiro Nishizawa, Tetsuya Gotou
特開2016-057978 状態遷移対応推定装置

Takeo Imai, Masahiro Sakai
US20160085816 A1 Information processing apparatus, information processing system, information processing method, and recording medium

Masahiro Sakai, Myungsook Ko, Eiichi Sunagawa, Takahiro Nishizawa, Tetsuya Gotou
特開2015-132539 日照量計算装置、経路提案装置および日照量計算方法

Yusuke Endoh, Hiromasa Shin, Mikito Iwamasa, Kohei Maruchi, Masahiro Sakai
特開2014-130414 テストパターンの生成装置、その生成方法及びその生成プログラム

Kohei Maruchi, Masahiro Sakai, Hiromasa Shin, Susumu Yoshizawa, Hirotaka Sakai, Yoshiyuki Nitta, Yukitaka Yoshida, Norihiro Umemura, Kanako Hattori
US 8,584,093 Pre-condition generation device, post-condition generation device, and method for generating these conditions

Masahiro Sakai, Takeo Imai
US 2012/0266133 A1 Precondition Generating Apparatus

Takeo Imai, Masahiro Sakai
特許5072889 事前条件生成装置および事後条件生成装置、ならびにこれらの方法

酒井, 政裕, 今井健
WO/2011/052030 Precondition Generating Apparatus

Takeo Imai, Masahiro Sakai
特開2009-157456 プログラム検証装置、プログラム検証方法、検証プログラム

丸地, 康平, 片岡, 欣夫, 酒井政
US 2009/0172643 A1 Program Verification Apparatus, Program Verification Method, and Program Storage Medium

Kohei Maruchi, Yoshio Kataoka, Masahiro Sakai