末永 幸平

J-GLOBALへ         更新日: 17/12/29 23:59
 
アバター
研究者氏名
末永 幸平
 
スエナガ コウヘイ
ハンドル
ksuenaga
URL
http://www.fos.kuis.kyoto-u.ac.jp/~ksuenaga/
所属
京都大学
職名
准教授
科研費研究者番号
70633692
Twitter ID
ksuenaga

プロフィール

2008年東京大学情報理工学系研究科コンピュータ科学専攻修了.博士(情報理工学).日本学術振興会特別研究員 (DC2, PD),日本アイ・ビー・エム(株)東京基礎研究所リサーチャー,リスボン大学理学部博士研究員,日本学術振興会特別研究員 (PD),京都大学白眉センター特定助教,を経て 2013年より京都大学大学院情報学研究科准教授.現在に至る.ソフトウェアシステム,ハイブリッドシステムの形式検証手法に興味を持つ.

異なる分野で使われている手法を形式検証の分野に持ち込んだり,形式検証のアイデアを他の分野に持ち込んだりするのが好きです.色んな分野の人と話をするのが好きです.

論文

 
末永 幸平
コンピュータソフトウェア = Computer software   34(1) 58-61   2017年2月
Hirofumi Nakamura, Kensuke Kojima, Kohei Suenaga and Atsushi Igarashi
APLAS 2017   514-533   2017年   [査読有り]
Masaki Waga,Ichiro Hasuo,Kohei Suenaga
Formal Modeling and Analysis of Timed Systems - 15th International Conference, FORMATS 2017, Berlin, Germany, September 5-7, 2017, Proceedings   224-243   2017年   [査読有り]
Taro Sekiyama,Akifumi Imanishi,Kohei Suenaga
CoRR   abs/1706.06462    2017年   [査読有り]
Masaki Waga,Ichiro Hasuo,Kohei Suenaga
CoRR   abs/1706.09174    2017年   [査読有り]
Takamasa Okudono,Yuki Nishida,Kensuke Kojima,Kohei Suenaga,Kengo Kido,Ichiro Hasuo
Programming Languages and Systems - 15th Asian Symposium, APLAS 2017, Suzhou, China, November 27-29, 2017, Proceedings   491-513   2017年   [査読有り]
Kensuke Kojima,Minoru Kinoshita,Kohei Suenaga
Static Analysis - 23rd International Symposium, SAS 2016, Edinburgh, UK, September 8-10, 2016, Proceedings   278-299   2016年   [査読有り]
Kensuke Kojima,Minoru Kinoshita,Kohei Suenaga
CoRR   abs/1604.07201    2016年   [査読有り]
園部 達也,末永 幸平,五十嵐 淳
Programming Languages and Systems 12th Asian Symposium, APLAS 2014, Singapore, Singapore, November 17-19, 2014, Proceedings, LNCS   8858 58-77   2014年11月   [査読有り]
赤崎 拓未,蓮尾 一郎,末永 幸平
Proc. of the 4th Workshop on Hybrid Autonomous Systems (HAS 2014)   22-39   2014年   [査読有り]
K. Suenaga; H. Sekine; I. Hasuo
Conference Record of the Annual ACM Symposium on Principles of Programming Languages   417-430   2013年   [査読有り]
K. Suenaga; R. Fukuda; A. Igarashi
Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA   1-20   2012年   [査読有り]
I. Hasuo; K. Suenaga
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)   7358 LNCS 462-478   2012年   [査読有り]
Ryosuke Sato,Kohei Suenaga,Naoki Kobayashi 0001
JIP   19 74-87   2011年   [査読有り]
K. Suenaga; I. Hasuo
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)   6756 LNCS(PART 2) 392-403   2011年   [査読有り]
佐藤 亮介, 末永 幸平, 小林 直樹
情報科学技術フォーラム講演論文集   8(1) 65-72   2009年8月
Suenaga et al. have developed a type-based framework for automatically translating tree-processing programs into stream-processing ones. The key ingredient of the framework was the use of ordered linear types to guarantee that a tree-processing pr...
K. Suenaga; N. Kobayashi
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)   5904 LNCS 128-143   2009年   [査読有り]
飯村 枝里, 小林 直樹, 末永 幸平
情報処理学会論文誌プログラミング(PRO)   1(2) 71-84   2008年9月
並行プログラムは,実行の非決定性などのために,バグが混入しやすく,またそのバグの発見が難しい.そこで,並行プログラムを静的かつ網羅的に検証するための手法として,型システムを用いた手法が近年注目されている.小林らはπ計算を対象としてデッドロックの検証を行う型システムを提案し,それに基づく自動検証器を実装している.しかしながら,型システムとそれに基づく検証アルゴリズムの複雑さのため,検証に失敗した場合に具体的にプログラムのどの部分に誤りがあるのかをユーザが判断するのは困難であった.本研究では,...
K. Kodama; K. Suenaga; N. Kobayashi
Journal of Functional Programming   18(3) 333-371   2008年   [査読有り]
Kohei Suenaga,Naoki Kobayashi 0001
Programming Languages and Systems, 16th European Symposium on Programming, ESOP 2007, Held as Part of the Joint European Conferences on Theory and Practics of Software, ETAPS 2007, Braga, Portugal, March 24 - April 1, 2007, Proceedings   490-504   2007年   [査読有り]
Naoki Kobayashi 0001,Kohei Suenaga,Lucian Wischik
Logical Methods in Computer Science   2(3)    2006年   [査読有り]
Naoki Kobayashi 0001,Kohei Suenaga,Lucian Wischik
Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings   298-312   2006年   [査読有り]
Naoki Kobayashi 0001,Kohei Suenaga,Lucian Wischik
CoRR   abs/cs/0608035    2006年   [査読有り]
Kohei Suenaga,Naoki Kobayashi 0001,Akinori Yonezawa
Logic Based Program Synthesis and Transformation, 15th International Symposium, LOPSTR 2005, London, UK, September 7-9, 2005, Revised Selected Papers   98-114   2005年   [査読有り]
Koichi Kodama,Kohei Suenaga,Naoki Kobayashi 0001
Programming Languages and Systems: Second Asian Symposium, APLAS 2004, Taipei, Taiwan, November 4-6, 2004. Proceedings   41-56   2004年   [査読有り]
Kohei Suenaga,Yutaka Oiwa,Eijiro Sumii,Akinori Yonezawa
Software Security - Theories and Systems, Second Mext-NSF-JSPS International Symposium, ISSS 2003, Tokyo, Japan, November 4-6, 2003, Revised Papers   192-208   2003年   [査読有り]
A Guess-and-Assume Approach to Loop Fusion for Program Verification
Akifumi Imanishi, Kohei Suenaga, Atsushi Igarashi
PEPM 2018      [査読有り]
CPSの形式検証——超準解析によるアプローチ
蓮尾 一郎,末永 幸平
計測と制御   53(12) 1-6   [査読有り][招待有り]

講演・口頭発表等

 
Towards Proof Synthesis by Neural Machine Translation
Taro Sekiyama, Akifumi Imanishi, Kohei Suenaga
Off the Beaten Track 2018 (OBT 2018)   2018年1月13日   
A Guess-and-Assume Approach to Loop Fusion for Program Verification
Akifumi Imanishi, Kohei Suenaga, Atsushi Igarashi
PEPM 2018   2018年1月8日   
A Guess-and-Assume Approach to Loop Fusion for Program Verification
Akifumi Imanishi, Kohei Suenaga, and Atsushi Igarashi
PEPM 2018   2018年1月7日   
超準プログラミング言語を用いたハイブリッドシステムのモデリングと検証 [招待有り]
末永 幸平
第9回 暗号及び情報セキュリティと数学の相関ワークショップ (CRISMATH 2017)   2017年12月22日   
Sharper and Simpler Nonlinear Interpolants for Program Verification
Takamasa Okudono, Yuki Nishida, Kensuke Kojima, Kohei Suenaga, Kengo Kido and Ichiro Hasuo
APLAS 2017   2017年11月27日   
A Nonstandard Functional Programming Language
Hirofumi Nakamura, Kensuke Kojima, Kohei Suenaga and Atsushi Igarashi.
APLAS 2017   2017年11月27日   
Efficient Online Timed Pattern Matching by Automata-Based Skipping
Masaki Waga, Ichiro Hasuo and Kohei Suenaga
15th International Conference on Formal Modelling and Analysis of Timed Systems   2017年9月5日   
Sharper and Simpler Nonlinear Interpolants for Program Verification
Takamasa Okudono, Yuki Nishida, Kensuke Kojima, Kohei Suenaga, Kengo Kido and Ichiro Hasuo
Workshop on Formal Approaches to Explainable VERification (FEVER 2017)   2017年7月23日   
Generalized Homogeneous Polynomials for Efficient Template-Based Nonlinear Invariant Synthesis
Kensuke Kojima, Minoru Kinoshita, and Kohei Suenaga
第19回プログラミングおよびプログラミング言語ワークショップ(PPL2017)   2017年3月8日   
無限状態システムのHFLモデル検査のための型に基づく手法
今井 雄毅, 小林 直樹, 佐藤 亮介, 末永 幸平, 塚田 武志
第19回プログラミングおよびプログラミング言語ワークショップ(PPL2017)   2017年3月8日   
深層学習によるプログラム生成の高速化
今西 諒文, 関山 太朗, 村主 崇行, 末永 幸平
第19回プログラミングおよびプログラミング言語ワークショップ(PPL2017)   2017年3月8日   
超準関数型プログラミング言語NSF
中村 博文, 末永 幸平, 五十嵐 淳, 小島 健介
第19回プログラミングおよびプログラミング言語ワークショップ(PPL2017)   2017年3月8日   
そのプログラム、バグってないですか?:数学を使ってバグを見つけるための形式検証手法 [招待有り]
末永 幸平
2016年度情報処理学会関西支部定期講演会「IoT の周辺技術」   2016年12月21日   
超準解析を用いたハイブリッドシステム検証手法 [招待有り]
末永 幸平
統計数理解析研究所シンポジウム --- 工学と現代数学の接点を求めて   2016年12月20日   
Generalized Homogeneous Polynomials for Efficient Template-Based Nonlinear Invariant Synthesis
末永 幸平
SAS 2016   2016年9月8日   
An Extended Behavioral Type System for Memory-Leak Freedom
Qi Tan, Kohei Suenaga, and Atsushi Igarashi
日本ソフトウェア科学会 第33回大会講演論文集   2016年9月7日   
ソフトウェアのための自動形式検証ツール
末永 幸平
ET/IoT 総合技術展 関西(ETWest 2016)   2016年7月7日   
そのプログラム、バグってないですか? ― 数学を使ってバグを見つける [招待有り]
末永 幸平
JST 京都大学新技術説明会   2016年5月24日   
Formal verification of software, continuous, and hybrid systems -- Or: How do we verify our program is correct?
末永 幸平
Machine Learning Summer School 2015   2015年8月27日   
Nonstandard Analysis Meets Programming Language Theory [招待有り]
末永 幸平
Twelfth International Conference on Computability and Complexity in Analysis   2015年7月13日   
Automatic Synthesis of Combiners in the MapReduce Framework
樹下 稔,末永 幸平,五十嵐 淳
24th International Symposium on Logic-Based Program Synthesis and Transformation   2014年9月9日   
Type-Based Safe Resource Deallocation for Shared-Memory Concurrency [招待有り]
末永 幸平
日本ソフトウェア科学会第30回大会特別招待講演   2013年9月12日   
末永 幸平
日本ソフトウェア科学会第30回大会Future Technology Design (FTD) 2013   2013年9月11日   
講演の様子は
https://www.youtube.com/watch?v=UydxhzofZl8
を参照のこと
Simulink blocks as stream processing ─ An approach from nonstandard analysis (Preliminary Report)
関根 大剛,末永 幸平,蓮尾 一郎
Fifth International Workshop on Numerical Software Verification (NSV 2012)   2012年7月7日   

受賞

 
2013年9月
京都大学 京都大学学際研究着想コンテスト優秀賞 視覚・聴覚に続く第三の電子媒体「匂い」--その時代に備えるための技術革新と社会環境整備
受賞者: 塩尻かおり,小石かつら,末永幸平,村主崇行,藤井啓祐
 
2012年6月
日本情報処理学会 Journal of Information Processing Outstanding Paper Award Ordered types for stream processing of tree-structured data. Journal of Information Processing
受賞者: 佐藤 亮介,末永 幸平,小林 直樹
 
2012年3月
日本ソフトウェア科学会プログラミング論研究会 PPL 2012 発表賞 Programming with infinitesimals: A WHILE-language for hybrid system modeling
受賞者: 末永 幸平,蓮尾 一郎
 
2009年3月
日本ソフトウェア科学会プログラミング論研究会 PPL 2009 発表賞 Type-based deadlock-freedom verification for non-block-structured lock primitives and mutable references
 
2007年3月
日本ソフトウェア科学会プログラミング論研究会 PPL 2007 発表賞 Type-based analysis of deadlock for a concurrent calculus with interrupts
受賞者: 末永 幸平,小林直樹
 

担当経験のある科目

 

委員歴

 
2017年6月
 - 
現在
PEPM 2018 プログラム委員
 
2015年3月
 - 
現在
情報処理学会関西支部  幹事
 
2013年7月
 - 
現在
文部科学省科学技術政策研究所科学技術動向研究センター  専門調査員
 
2012年2月
 - 
現在
情報処理学会  若手研究者の会
 
 
 - 
現在
PPL 2017 プログラム委員
 

競争的資金等の研究課題

 
ハイブリッドシステムのための超準プログラミング言語理論を用いた形式手法
JST: さきがけ
研究期間: 2015年10月 - 2018年3月    代表者: 末永 幸平
文部科学省: 科学研究費補助金(若手研究(B))
研究期間: 2013年 - 2015年    代表者: 末永 幸平
文部科学省: 科学研究費補助金(研究活動スタート支援)
研究期間: 2012年 - 2013年    代表者: 末永 幸平
前年度に提案した無限小プログラミングのための検証のフレームワークに基づいて無限小プログラムのホーア論理に基づく検証手法を提案し実装した.本実装は (1) バックエンドにおいて既存の自動定理証明器を拡張なしに用いることができるという点 (2) 既存研究でソフトウェアのための形式検証手法として提案された手法をそのまま用いることができる点に特徴がある.本研究は,ハイブリッドシステムの検証手法として無限小プログラミングの枠組みを利用するための重要なステップである.提案手法の理論的枠組と本実装に基づ...
並行プログラムのための型理論に基づく利便性の高い静的検証手法
日本学術振興会: 科研費・特別研究員奨励費
研究期間: 2011年4月 - 2012年3月    代表者: 末永 幸平
並行プログラム検証のための型システムとそのオペレーティングシステムの検証への応用
日本学術振興会: 科研費・特別研究員奨励費
研究期間: 2007年4月 - 2009年3月    代表者: 末永 幸平

特許

 
特願2017-246154 : プログラム検証装置、プログラム検証方法、プログラム検証のためのコンピュータプログラム、プログラム変換器、プログラム変換方法、プログラム変換のためのコンピュータプログラム、プログラム製造方法、及び検証用プログラム
末永 幸平, 今西 諒文, 五十嵐 淳
特願2017-137949 : 自動証明装置、及びプログラム
蓮尾 一郎,奥殿 貴仁,木戸 肩吾,末永 幸平,小島 健介,西田 雄気
PCT/JP2017/003295 : 不変条件生成装置、コンピュータプログラム、不変条件生成方法、プログラムコード製造方法
樹下稔,小島健介,末永幸平
特願2014-72623 : 制御入力値生成装置,制御入力値生成方法,および,プログラム
赤崎 拓未,蓮尾 一郎,末永 幸平
特許8766980 : Information management system, method and program
宮下尚,中村宏明,末永幸平

経歴

 
2017年6月
 - 
現在
Patentfield 株式会社 科学技術顧問
 
2013年10月
 - 
現在
京都大学 大学院情報学研究科 准教授
 
2012年4月
 - 
2013年9月
京都大学 白眉センター 特定助教
 
2011年4月
 - 
2012年3月
日本学術振興会 特別研究員 (PD)
 
2011年2月
 - 
2011年3月
京都大学 大学院情報学研究科 特定研究員
 

学歴

 
2005年4月
 - 
2008年3月
東京大学 大学院情報理工学系研究科 コンピュータ科学専攻博士課程
 
2003年4月
 - 
2005年3月
東京大学 大学院情報理工学系研究科 コンピュータ科学専攻修士課程
 
2000年4月
 - 
2003年3月
東京大学 理学部 情報科学科
 
1998年4月
 - 
2000年3月
東京大学 教養学部 理科一類
 
1995年4月
 - 
1998年3月
宮崎県立宮崎西高等学校  理数科
 

所属学協会

 
 

その他

 
2014年4月   自動車企業との共同研究
自動車設計における形式手法適用について自動車企業との関連研究を行っております.

研究分野