Masahiro Sakai

株式会社Preferred Networks / Engineer

Masahiro Sakai

株式会社Preferred Networks / Engineer

Masahiro Sakai

株式会社Preferred Networks / Engineer

This user is using the new profile.

Join our Beta test to try out our new profile.

Join

2007 年 慶應義塾大学大学院政策・メディア研究科修士課程了。 電機メーカの研究部門にて 形式手法、ソフトウェアテストなどのソフトウェア高信頼化の研究に従事した後、現在は Preferred Networks, Inc. にてエンジニアとして働く。 関数型プログラミングや理論計算機科学に興味を持つ。 訳書(共訳)に『抽象によるソフトウェア設計−Alloyではじめる形式手法−』、『型システム入門−プログラミング言語と型の理論−』。

May 2017
-
Present

Engineer
Present

May 2017 -

Present

Apr 2007
-
Apr 2017

東芝

11 years

研究者

Apr 2007 - Apr 2017

I worked as a researcher for System Engineering Laboratory, Toshiba Research and Development Center. I have worked in software dependability team to develop technology based on formal methods, program analysis, automatic test-case generation to achieve more dependable systems. I have also worked in cities infrastructure solutions team and developed a recommendation system that recommends brick-and-mortar shops/goods on smart-phone for regional promotion.

抽象によるソフトウェア設計 ―Alloyではじめる形式手法

July 2011

抽象によるソフトウェア設計 ―Alloyではじめる形式手法

July 2011

SAT問題と他の制約問題との相互発展

Jan 2015

SAT問題と他の制約問題との相互発展

Jan 2015

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

Mar 2013

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

Mar 2013

Minimal Unsatisfiable Core列挙によるプログラムの準最弱な事前条件推定

Aug 2013

Minimal Unsatisfiable Core列挙によるプログラムの準最弱な事前条件推定

Aug 2013

MC/DC-like Structural Coverage Criteria for Function Block Diagrams

Mar 2014

MC/DC-like Structural Coverage Criteria for Function Block Diagrams

Mar 2014

Model-checking C programs against JML-like specification language

Dec 2012

Model-checking C programs against JML-like specification language

Dec 2012

Kawasaki Grand City Mall

Toshiba carried a demonstration experiment on smart city and O2O service around Kawasaki Station (c.f. http://www.toshiba.co.jp/about/press/2013_12/pr_j1901.htm http://www.city.kawasaki.jp/200/page/0000053904.html (written in Japanese)). As part of this experiment, we have developed a recommendation system that recommends brick-and-mortar shops/goods on smart-phone for regional promotion. I leaded a team for data analysis and recommendation algorithm development.

Kawasaki Grand City Mall

Toshiba carried a demonstration experiment on smart city and O2O service around Kawasaki Station (c.f. http://www.toshiba.co.jp/about/press/2013_12/pr_j1901.htm http://www.city.kawasaki.jp/200/page/0000053904.html (written in Japanese)). As part of this experiment, we have developed a recommendation system that recommends brick-and-mortar shops/goods on smart-phone for regional promotion. I leaded a team for data analysis and recommendation algorithm development.

toysolver / toysat

Solver implementation of various problems including SAT, Max-SAT, PBS (Pseudo Boolean Satisfaction), PBO (Pseudo Boolean Optimization), MILP (Mixed Integer Linear Programming) and non-linear real arithmetic. In particular It contains a moderately-fast pure-Haskell SAT solver 'toysat'. I submitted it to solver competitions (Pseudo Boolean Competition and Max-SAT Evaluations) and ranked high in some competition categories.

toysolver / toysat

Solver implementation of various problems including SAT, Max-SAT, PBS (Pseudo Boolean Satisfaction), PBO (Pseudo Boolean Optimization), MILP (Mixed Integer Linear Programming) and non-linear real arithmetic. In particular It contains a moderately-fast pure-Haskell SAT solver 'toysat'. I submitted it to solver competitions (Pseudo Boolean Competition and Max-SAT Evaluations) and ranked high in some competition categories.

Ruby-GNOME2

Ruby-GNOME2 is a set of Ruby language bindings for the GNOME >=2.0 development environment. I was one of core developers in the early days. In particular I have designed/wrote a general bridge between Ruby's object system and GObject object system using reflection/introspection features and replaced non-extensible hard-coded one in its predecessor Ruby/GTK1.

Ruby-GNOME2

Ruby-GNOME2 is a set of Ruby language bindings for the GNOME >=2.0 development environment. I was one of core developers in the early days. In particular I have designed/wrote a general bridge between Ruby's object system and GObject object system using reflection/introspection features and replaced non-extensible hard-coded one in its predecessor Ruby/GTK1.

CPL : A categorical programming language interpreter

I implemented an interpreter of CPL, a functional programming language based on category theory, designed by Prof. Tatsuya Hagino. In CPL, data types are declared in a categorical manner by adjunctions. Each data type is declared with its basic operations or morphisms. Programs consist of these morphisms, and execution of programs is the reduction of elements (i.e. special morphisms) to their canonical form. http://hackage.haskell.org/package/CPL https://github.com/msakai/cpl

CPL : A categorical programming language interpreter

I implemented an interpreter of CPL, a functional programming language based on category theory, designed by Prof. Tatsuya Hagino. In CPL, data types are declared in a categorical manner by adjunctions. Each data type is declared with its basic operations or morphisms. Programs consist of these morphisms, and execution of programs is the reduction of elements (i.e. special morphisms) to their canonical form. http://hackage.haskell.org/package/CPL https://github.com/msakai/cpl

CForge: Bounded model checker for C language.

CForge is a C program analyzer based on a program analysis framework Forge developed by the Software Design Group (SDG) at MIT, and we developed CForge as part of a joint research project with MIT SDG. I worked as a main developper of CForge, and worked on its overall design, design of our formal specification langauge for C, implementaion of a kind of C compiler, and so on. http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6462652 http://www.toshiba.co.jp/tech/review/2009/08/64_08pdf/a06.pdf

CForge: Bounded model checker for C language.

CForge is a C program analyzer based on a program analysis framework Forge developed by the Software Design Group (SDG) at MIT, and we developed CForge as part of a joint research project with MIT SDG. I worked as a main developper of CForge, and worked on its overall design, design of our formal specification langauge for C, implementaion of a kind of C compiler, and so on. http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6462652 http://www.toshiba.co.jp/tech/review/2009/08/64_08pdf/a06.pdf

Economic load dispatch

Economic load dispatch is the determination of the output of electricity generation units, that meet the electricity demands with lowest possible cost, subject to complex operational constraints. I assisted research project of economic load dispatch problem by removing performance bottlenecks of our prototype optimization system, setting up continuous integration environment, and writing minor modules of the system. My work is partly applied to the system for TEPCO Fuel & Power, Incorporated. http://www3.toshiba.co.jp/power/whatsnew/topics/20161026/index_j.htm http://www.toshiba.co.jp/tech/review/2016/03/71_03pdf/0A.pdf#page=6

Economic load dispatch

Economic load dispatch is the determination of the output of electricity generation units, that meet the electricity demands with lowest possible cost, subject to complex operational constraints. I assisted research project of economic load dispatch problem by removing performance bottlenecks of our prototype optimization system, setting up continuous integration environment, and writing minor modules of the system. My work is partly applied to the system for TEPCO Fuel & Power, Incorporated. http://www3.toshiba.co.jp/power/whatsnew/topics/20161026/index_j.htm http://www.toshiba.co.jp/tech/review/2016/03/71_03pdf/0A.pdf#page=6

PTQ : An implementation of Montague's PTQ in Haskell

Montague grammer and the PTQ (The Proper Treatment of Quantification in Ordinary English) by Richard Montague were pioneering work in the field of formal semantics of natural languages, and showed that natural languages (like English) and formal languages (like programming languages) can be treated in the similar way. I implemented his theory in interactive environment. http://hackage.haskell.org/package/PTQ https://github.com/msakai/ptq

PTQ : An implementation of Montague's PTQ in Haskell

Montague grammer and the PTQ (The Proper Treatment of Quantification in Ordinary English) by Richard Montague were pioneering work in the field of formal semantics of natural languages, and showed that natural languages (like English) and formal languages (like programming languages) can be treated in the similar way. I implemented his theory in interactive environment. http://hackage.haskell.org/package/PTQ https://github.com/msakai/ptq

2007

Keio University

Graduate School of Media and Governance

2007

非正格関数に対して適用可能な融合変換

Jan 2007

非正格関数に対して適用可能な融合変換

Jan 2007

Faculty of Policy Management

2000

Shonan High School

2000


Skills and qualities

数理計画

Recommended by Takeo Imai, Michiaki Ariga
2

Alloy

Recommended by Takeo Imai
1

継続的統合

Recommended by Shuichiro Imahara
1

Continuous Integration

Recommended by Shuichiro Imahara
1

Haskell

Recommended by Takeo Imai
1

Publications

SAT問題と他の制約問題との相互発展

Jan 2015

MC/DC-like Structural Coverage Criteria for Function Block Diagrams

Mar 2014

Minimal Unsatisfiable Core列挙によるプログラムの準最弱な事前条件推定

Aug 2013

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

Mar 2013

Model-checking C programs against JML-like specification language

Dec 2012

Show more

Accomplishments/Portfolio

Economic load dispatch

Ruby-GNOME2

CPL : A categorical programming language interpreter

PTQ : An implementation of Montague's PTQ in Haskell

toysolver / toysat

Show more


Languages

English - Professional, Japanese - Native