MASAHIRO SAKAI (酒井 政裕) ― Research and Development Engineer
- Email : email@example.com
- Web : http://msakai.jp
- LinkedIn : https://www.linkedin.com/in/masahirosakai
- GitHub : https://github.com/msakai
Masahiro Sakai is a researcher in the field of theoretical computer science. He is working as a software engineer at Preferred Networks, Inc. He received a master degree in “Media and Governance” with “Cyber Informatics” concentration at Keio university. He translated “Software Abstractions” and “Types and Programming Languages” into Japanese with his colleagues.
He is passionate in learning new technologies / skills / knowledge and putting them in practice by writing code, and he strives hard toward perfection.
His interest includes Programming Language Theory, Functional Programming, Software Engineering, Category Theory, Constraint Solving, SAT/SMT Solvers, Machine Learning, Mathematical Optimization, and Computer Security.
Engineer (May 2017 to Present)
Engineer (Apr 2007 to June 2015) and Research Scientist (July 2015 to April 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, and 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.
Economic load dispatch (2015-2016):
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 heuristic algorithm and minor modules of the system. My work is partly applied to the system for TEPCO Fuel & Power, Incorporated. (c.f. 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 (written in Japanese))
Recommendation system for Kawasaki Grand City Mall project (2013-2015):
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.
SMT-based semi-automatic test-case generation for power plant control systems (2010-2014):
Power plant controllers are often programmed using graphical data flow language such as Function Block Diagram (FBD). We have proposed new test coverage criteria for FBD and developed technology to automatically generate test cases that satisfy the proposed criteria. I developed core algorithms of our approach that encodes both FBD programs and conditions for proposed criteria into logical formula and solves the conjoined formula using SMT solvers to generate test cases.
I assisted language/runtime design of “Molatomium”, a parallel programming model for “Cell Broadband Engine”-like heterogeneous multicore processors, which was shipped with Toshiba's flagship digital TV “CELL REGZA”. (c.f. https://www.usenix.org/conference/hotpar-10/molatomium-parallel-programming-model-practice )
Specification mining based on UNSAT core enumeration (2008-):
Specification mining tackles the software maintenance and reliability issues by mining latent specification from source code. We have developed novel technology to mine pre-condition (one type of specification) by combining model checking and minimal unsatisfiable core enumeration.
CForge: Bounded model checker for C language (2008-2012):
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 developer of CForge, and worked on its overall design, design of our formal specification language for C, implementation of a kind of C compiler, and so on.
Verification of work-flow networks based on model checking (2007).
- Engineering Knowledge and Interests:
- Functional Programming, Language Design, Formal Methods, Model Checking, SAT/SMT solvers, Machine Learning, Recommendation System, Mathematical Optimization, Category Theory, Type Theory, Logic.
- Programming Languages:
- Haskell, Ruby, Python, Java, C.
- Japanese: Native Speaker
- English: Professional Proficiency
- Process Mining: Data science in Action (May. 2015) by Prof. Wil van der Aalst, Eindhoven University of Technology
- Discrete Optimization (May. 2015) by Prof. Pascal Van Hentenryck, The University of Melbourne
- Gamification (Mar. 2015) by Assoc. Prof. Kevin Werbach, University of Pennsylvania
- Heterogeneous Parallel Programming (Mar. 2014) by Prof. Wen-mei W. Hwu, University of Illinois at Urbana-Champaign
- Introduction to Recommender Systems (Dec. 2013) by Prof. Joseph A. Konstan and Assist. Prof. Michael D. Ekstrand, University of Minnesota
- Maps and the Geospatial Revolution (Aug. 2013) by Assist. Prof. Anthony C. Robinson, The Pennsylvania State University
- Developing Innovative Ideas for New Companies: The First Step in Entrepreneurship (May. 2013) by Dr. James V. Green, University of Maryland, College Park
- Model Thinking (Aug. 2013) by Prof. Scott E. Page, University of Michigan
- Machine Learning (Jul. 2013) by Assoc. Prof. Andrew Ng, Stanford University
- Linear and Discrete Optimization (Apr. 2013) by Prof. Friedrich Eisenbrand, École Polytechnique Fédérale de Lausanne
- Data Analysis (Mar. 2013) by Assist. Prof. Jeff Leek, Johns Hopkins University
- Computing for Data Analysis (Jan. 2013) by Assoc. Prof. Roger D. Peng, Johns Hopkins University
TOEIC Score 960 (Listening: 470; Reading: 470) (Mar. 2018)
C言語ベースの組込みハードウェア設計 (A course on C-based design of embedded hardware) (Oct. 2007) by NEXCESS (Nagoya University Extension Courses for Embedded Software Specialists).
March 2007: Master of Media and Governance (Course: Cyber Informatics), Graduate School of Media and Governance, Keio University.
- Master thesis: "Fusion Transformations Applicable to Non-Strict Functions" ("非正格関数に対して適用可能な融合変換"). Adviser: Prof. Tatsuya Hagino.
March 2005: Bachelor of Arts in Policy Management, Faculty of Policy Management, Keio University.
Books and Selected Publications
Benjamin C. Pierce, Eijiro Sumii, Yusuke Endoh, Masahiro Sakai, Keigo Imai, Yusuke Kuroki, Yoshihiro Imai, Takafumi Saikawa and Takeo Imai, “型システム入門－プログラミング言語と型の理論－” (Japanese translation of “Types and Programming Languages”). Ohmsha, 2013. ISBN: 978-4-274-06911-6
Daniel Jackson, Shin Nakajima, Takeo Imai, Masahiro Sakai, Yusuke Endoh and Yoshio Kataoka, “抽象によるソフトウェア設計－Alloyではじめる形式手法” (Japanese translation of “Software Abstractions: Logic, Language, and Analysis”). Ohmsha, 2011. ISBN: 978-4-274-06858-4
Masahiro Sakai and Takeo Imai, “Interplay between SAT and other Constraint Problems,” Computer Software, Vol. 32, No. 1, 2015, pp. 103-119. doi:10.11309/jssst.32.1_103 https://www.jstage.jst.go.jp/article/jssst/32/1/32_1_103/_article/-char/en/
Kohei Maruchi, Hiromasa Shin and Masahiro Sakai, "MC/DC-like Structural Coverage Criteria for Function Block Diagrams," In proceedings of Software Testing, Verification and Validation Workshops (ICSTW). Cleveland, Ohio USA, 2014. pp. 253-259. doi:10.1109/ICSTW.2014.27 http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6825670
Takeo Imai, Masahiro Sakai, Masami Hagiya, “An Inference Method of Quasi-Weakest Preconditions by Minimal Unsatisfiable Core Enumeration,” Computer Software, Vol. 30, No. 2, 2013, pp. 207-226. doi:10.11309/jssst.30.2_207 https://www.jstage.jst.go.jp/article/jssst/30/2/30_2_207/_article/-char/en/
Masahiro Sakai, Kohei Maruchi and Takeo Imai, "Model-checking C programs against JML-like specification language," in Proceedings of the 19th Asia-Pacific Software Engineering Conference (APSEC2012), Hong Kong, 2012, pp. 174-183. doi:10.1109/APSEC.2012.68 http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6462652
Masahiro Sakai, "Fusion Transformations Applicable to Non-Strict Functions," ("非正格関数に対して適用可能な融合変換,") Master thesis, Graduate School of Media and Governance, Keio University, Jan. 2007.
Recognition and Awards
- 2017 (社内表彰): 株式会社東芝 研究開発センター 業績賞優秀賞 (平成29年4月6日)
- 2015: the 19th Research Paper Award from Japan Society for Software Science and Technology for the paper “An Inference Method of Quasi-Weakest Preconditions by Minimal Unsatisfiable Core Enumeration” (日本ソフトウェア科学会第19回研究論文賞)
- 2014 (社内表彰): 株式会社東芝 コミュニティ・ソリューション社 知的財産活動奨励賞 (平成26年7月7日)
External reviewer of IPSJ/SIGSE Software Engineering Symposiums (SES2014, SES2015).
Reviewed some technical books (about computer science and functional programming) before publication:
Graham Hutton and Kazuhiko Yamamoto, “プログラミングHaskell” (Japanese translation of “Programming in Haskell”), Ohmsha, 2009. ISBN: 978-4274067815
Jeremy Gibbons, Oege de Moor and Nobuo Yamashita, “関数プログラミングの楽しみ”(Japanese translation of “the fun of programming”), Ohmsha, 2010. ISBN: 978-4274068058
Richard Bird and Nobuo Yamashita, “関数プログラミング入門 ― Haskellで学ぶ原理と技法―” (Japanese translation of “Introduction to Functional Programming with Haskell), Ohmsha, 2012. IBSN: 978-4274068966
Tom Stuart, Koichi Saasda and Takashi Sasai, “アンダースタン ディング コンピュテーション--単純な機械から不可能なプログラムまで” (Japanese translation of “Understanding Computation -- From Simple Machines to Impossible Programs”), O'Reilly Japan, 2014. ISBN: 978-4873116976
Richard Bird and Nobuo Yamashita, “関数プログラミング 珠玉の アルゴリズムデザイン” (Japanese translation of “Pearls of Functional Algorithm Design”), Ohmsha, 2014. ISBN: 978-4274050640
Mark C. Chu-Carroll and cocoatomo, “グッド・マス ギークのための数・論理・計算機科学” (Japanese translation of “Good Math: A Geek's Guide to the Beauty of Numbers, Logic, and Computation”), Ohmsha, 2016. ISBN: 978-4-274-21896-5
Open Source Activities
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 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.
PTQ : An implementation of Montague's PTQ in Haskell
Montague grammar 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.
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.
Google Code Jam Japan 2011: 44th place among 918 participants
Computer security competitions (CTF; Capture the Flag)
- CTF for beginners 2015 Tokyo: 6th place among 103 participants
- Trend Micro CTF Asia Pacific & Japan 2015 Online Qualifier: 46th place among 881 teams, as a team "Ten*48"
- SECCON 2015 Online CTF: 43th place among 1251 teams, as a team "Ten*48"
- DEF CON CTF Qualifier 2016: 164th place among 1335 teams, as a team "Ten*48"
- HITCON CTF 2016 Quals: 34th place among 1024 teams, as a team "Ten*48"
Study group of category theory (圏論勉強会): 2004 - 2012
Category theory is a highly general and abstract mathematical theory, which has applications not only in mathematics but also in theoretical computer science, functional programming, physics, linguistics and many other fields. I was one of core members of the study group and we had studied following materials:
- “Conceptual Mathematics: A First Introduction to Categories” by F. William Lawvere and Stephen Hoel Schanuel,
- “Categories, Types, and Structures: An Introduction to Category Theory for the Working Computer Scientist” by Andrea Asperti and Giuseppe Longo,
- “The Haskell Programmer's Guide to the IO Monad — Don't Panic” by Stefan Klinger,
- “Temperley-Lieb Algebra: From Knot Theory to Logic and Computation via Quantum Mechanics” by Samson Abramsky
- “A survey of graphical languages for monoidal categories” by Peter Selinger
- “Categorical Logic and Type Theory” by Bart Jacobs.
There is a Japanese article about this study group: “Technical Study Session Map in Japan - Join a Live Session of Engineers!”, 情報処理, Vol.52, No.4, Apr. 2011. http://id.nii.ac.jp/1001/00073853/
RHG reading group (RHG読書会): 2003 - 2009
This study group was a group of programming language geeks. It was started initially as a study group of reading “Rubyソースコード完全解説” (known as “Ruby Hacking Guide”), but eventually we have studied many programming and programming language related books/materials:
- YARV (Ruby >=1.9 VM),
- なでしこ (a Japanese programming language),
- “実践Common Lisp” (Japanese translation of “Practical Common Lisp”),
- 2014-2015: Toshiba Systems & Software Institute
- Feb. 2006: ベトナム高度IT教育者実践研修
- Aug. 2003 - Sep. 2003: ITスキル標準人材育成研修