末永 幸平

最終更新日時: 2018/06/27 15:51:41

印刷する

氏名(漢字/フリガナ/アルファベット表記)
末永 幸平/スエナガ コウヘイ/Kohei Suenaga
所属部署・職名(部局/所属/講座等/職名)
情報学研究科/通信情報システム専攻コンピュータ工学講座/准教授
学部兼担
部局 所属 講座等 職名
工学部 工学部
取得学位
学位名(日本語) 学位名(英語) 大学(日本語) 大学(英語) 取得区分
修士(情報理工学) 東京大学
博士(情報理工学) 東京大学
出身大学院・研究科等
大学名(日本語) 大学名(英語) 研究科名(日本語) 研究科名(英語) 専攻名(日本語) 専攻名(英語) 修了区分
東京大学 大学院情報理工学系研究科コンピュータ科学専攻修士課程 修了
東京大学 大学院情報理工学系研究科コンピュータ科学専攻博士課程 修了
出身学校・専攻等
大学名(日本語) 大学名(英語) 学部名(日本語) 学部名(英語) 学科名(日本語) 学科名(英語) 卒業区分
東京大学 理学部情報科学科 卒業
東京大学 教養学部理科一類
出身高等学校
高等学校名 ふりがな
宮崎県立宮崎西高等学校 みやざきけんりつみやざきにしこうとうがっこう
職歴
期間 組織名(日本語) 組織名(英語) 職名(日本語) 職名(英語)
2007/04/01〜2008/03/31 日本学術振興会 JSPS 特別研究員 (DC2) Research Fello (DC2)
2008/04/01〜2009/03/31 日本学術振興会 JSPS 特別研究員 (PD) Research Fellow (PD)
2009/04/01〜2010/03/31 日本アイ・ビー・エム(株)東京基礎研究所 IBM Research Tokyo リサーチャー Researcher
2010/04/01〜2011/01/31 リスボン大学理学部 Faculdade de Ciencia, Universidade de Lisboa 博士研究員 Investigador pos-doutorado
2011/02/01〜2011/03/31 京都大学情報学研究科 Department of Informatics, Kyoto University 特定研究員 Researcher
2011/04/01〜2012/03/31 日本学術振興会 JSPS 特別研究員 (PD) Research Fellow (PD)
2012/04/01〜2013/09/30 京都大学白眉センター The Hakubi Center for Advanced Reserach, Kyoto University 特定助教 Assistant Professor
2015/10/01〜 科学技術振興機構 JST さきがけ研究者(兼任)
2017/06/01〜 Patentfield株式会社 Patentfield Inc. 科学技術顧問 Scientific Advisor
研究テーマ
(日本語)
プログラム検証,特にハイブリッドシステム(連続的遷移と離散的遷移が共存するシステム)の形式検証.
(英語)
Program verification; formal verification for hybrid systems (i.e., systems that exhibit both discrete and continuous behavior) especially.
研究分野(キーワード)
キーワード(日本語) キーワード(英語)
ソフトウェア software
ハイブリッドシステム hybrid systems
プログラム検証 program verification
形式手法 formal methods
プログラミング言語理論 theory of programming languages
研究分野(科研費分類コード)
科研費分類コード
ソフトウエア
情報学基礎
論文
著者 著者(日本語) 著者(英語) タイトル タイトル(日本語) タイトル(英語) 書誌情報等 書誌情報等(日本語) 書誌情報等(英語) 出版年月 査読の有無 記述言語 掲載種別 公開
Akifumi Imanishi, Kohei Suenaga, Atsushi Igarashi Akifumi Imanishi, Kohei Suenaga, Atsushi Igarashi Akifumi Imanishi, Kohei Suenaga, Atsushi Igarashi A Guess-and-Assume Approach to Loop Fusion for Program Verification A Guess-and-Assume Approach to Loop Fusion for Program Verification A Guess-and-Assume Approach to Loop Fusion for Program Verification PEPM 2018,2-14 PEPM 2018,2-14 PEPM 2018,2-14 2018 英語 研究論文(国際会議プロシーディングス) 公開
末永 幸平 末永 幸平 末永 幸平 PLDI 2016参加報告 PLDI 2016参加報告 PLDI 2016 Report コンピュータソフトウェア = Computer software,34,1,58-61 コンピュータソフトウェア = Computer software,34,1,58-61 コンピュータソフトウェア = Computer software,34,1,58-61 2017/02 日本語 公開
Takamasa Okudono,Yuki Nishida,Kensuke Kojima,Kohei Suenaga,Kengo Kido,Ichiro Hasuo Takamasa Okudono,Yuki Nishida,Kensuke Kojima,Kohei Suenaga,Kengo Kido,Ichiro Hasuo Takamasa Okudono,Yuki Nishida,Kensuke Kojima,Kohei Suenaga,Kengo Kido,Ichiro Hasuo Sharper and Simpler Nonlinear Interpolants for Program Verification. Sharper and Simpler Nonlinear Interpolants for Program Verification. Sharper and Simpler Nonlinear Interpolants for Program Verification. Programming Languages and Systems - 15th Asian Symposium, APLAS 2017, Suzhou, China, November 27-29, 2017, Proceedings,491-513 Programming Languages and Systems - 15th Asian Symposium, APLAS 2017, Suzhou, China, November 27-29, 2017, Proceedings,491-513 Programming Languages and Systems - 15th Asian Symposium, APLAS 2017, Suzhou, China, November 27-29, 2017, Proceedings,491-513 2017 公開
Masaki Waga,Ichiro Hasuo,Kohei Suenaga Masaki Waga,Ichiro Hasuo,Kohei Suenaga Masaki Waga,Ichiro Hasuo,Kohei Suenaga Efficient Online Timed Pattern Matching by Automata-Based Skipping. Efficient Online Timed Pattern Matching by Automata-Based Skipping. Efficient Online Timed Pattern Matching by Automata-Based Skipping. Formal Modeling and Analysis of Timed Systems - 15th International Conference, FORMATS 2017, Berlin, Germany, September 5-7, 2017, Proceedings,224-243 Formal Modeling and Analysis of Timed Systems - 15th International Conference, FORMATS 2017, Berlin, Germany, September 5-7, 2017, Proceedings,224-243 Formal Modeling and Analysis of Timed Systems - 15th International Conference, FORMATS 2017, Berlin, Germany, September 5-7, 2017, Proceedings,224-243 2017 公開
Takamasa Okudono,Yuki Nishida,Kensuke Kojima,Kohei Suenaga,Kengo Kido,Ichiro Hasuo Takamasa Okudono,Yuki Nishida,Kensuke Kojima,Kohei Suenaga,Kengo Kido,Ichiro Hasuo Takamasa Okudono,Yuki Nishida,Kensuke Kojima,Kohei Suenaga,Kengo Kido,Ichiro Hasuo Sharper and Simpler Nonlinear Interpolants for Program Verification. Sharper and Simpler Nonlinear Interpolants for Program Verification. Sharper and Simpler Nonlinear Interpolants for Program Verification. CoRR,abs/1709.00314 CoRR,abs/1709.00314 CoRR,abs/1709.00314 2017 公開
Taro Sekiyama,Akifumi Imanishi,Kohei Suenaga Taro Sekiyama,Akifumi Imanishi,Kohei Suenaga Taro Sekiyama,Akifumi Imanishi,Kohei Suenaga Towards Proof Synthesis Guided by Neural Machine Translation for Intuitionistic Propositional Logic. Towards Proof Synthesis Guided by Neural Machine Translation for Intuitionistic Propositional Logic. Towards Proof Synthesis Guided by Neural Machine Translation for Intuitionistic Propositional Logic. CoRR,abs/1706.06462 CoRR,abs/1706.06462 CoRR,abs/1706.06462 2017 公開
Hirofumi Nakamura, Kensuke Kojima, Kohei Suenaga and Atsushi Igarashi Hirofumi Nakamura, Kensuke Kojima, Kohei Suenaga and Atsushi Igarashi Hirofumi Nakamura, Kensuke Kojima, Kohei Suenaga and Atsushi Igarashi A Nonstandard Functional Programming Language A Nonstandard Functional Programming Language A Nonstandard Functional Programming Language APLAS 2017,514-533 APLAS 2017,514-533 APLAS 2017,514-533 2017 英語 研究論文(国際会議プロシーディングス) 公開
Masaki Waga,Ichiro Hasuo,Kohei Suenaga Masaki Waga,Ichiro Hasuo,Kohei Suenaga Masaki Waga,Ichiro Hasuo,Kohei Suenaga Efficient Online Timed Pattern Matching by Automata-Based Skipping. Efficient Online Timed Pattern Matching by Automata-Based Skipping. Efficient Online Timed Pattern Matching by Automata-Based Skipping. CoRR,abs/1706.09174 CoRR,abs/1706.09174 CoRR,abs/1706.09174 2017 公開
Kensuke Kojima,Minoru Kinoshita,Kohei Suenaga Kensuke Kojima,Minoru Kinoshita,Kohei Suenaga Kensuke Kojima,Minoru Kinoshita,Kohei Suenaga Generalized Homogeneous Polynomials for Efficient Template-Based Nonlinear Invariant Synthesis. Generalized Homogeneous Polynomials for Efficient Template-Based Nonlinear Invariant Synthesis. Generalized Homogeneous Polynomials for Efficient Template-Based Nonlinear Invariant Synthesis. Static Analysis - 23rd International Symposium, SAS 2016, Edinburgh, UK, September 8-10, 2016, Proceedings,9837 LNCS,278-299 Static Analysis - 23rd International Symposium, SAS 2016, Edinburgh, UK, September 8-10, 2016, Proceedings,9837 LNCS,278-299 Static Analysis - 23rd International Symposium, SAS 2016, Edinburgh, UK, September 8-10, 2016, Proceedings,9837 LNCS,278-299 2016 英語 研究論文(学術雑誌) 公開
Kensuke Kojima,Minoru Kinoshita,Kohei Suenaga Kensuke Kojima,Minoru Kinoshita,Kohei Suenaga Kensuke Kojima,Minoru Kinoshita,Kohei Suenaga Generalized Homogeneous Polynomials for Efficient Template-Based Nonlinear Invariant Synthesis. Generalized Homogeneous Polynomials for Efficient Template-Based Nonlinear Invariant Synthesis. Generalized Homogeneous Polynomials for Efficient Template-Based Nonlinear Invariant Synthesis. CoRR,abs/1604.07201 CoRR,abs/1604.07201 CoRR,abs/1604.07201 2016 公開
Daisuke Ishii,Kohei Suenaga,Walid Taha Daisuke Ishii,Kohei Suenaga,Walid Taha Daisuke Ishii,Kohei Suenaga,Walid Taha Validated Numerics Meets Reachability Analysis for CPS Design (NII Shonan Meeting 2015-14). Validated Numerics Meets Reachability Analysis for CPS Design (NII Shonan Meeting 2015-14). Validated Numerics Meets Reachability Analysis for CPS Design (NII Shonan Meeting 2015-14). NII Shonan Meet. Rep.,2015 NII Shonan Meet. Rep.,2015 NII Shonan Meet. Rep.,2015 2015 公開
園部 達也,末永 幸平,五十嵐 淳 園部 達也,末永 幸平,五十嵐 淳 Tatsuya Sonobe, Kohei Suenaga, and Atsushi Igarashi Automatic Memory Management Based on Program Transformation Using Ownership Automatic Memory Management Based on Program Transformation Using Ownership Automatic Memory Management Based on Program Transformation Using Ownership Programming Languages and Systems 12th Asian Symposium, APLAS 2014, Singapore, Singapore, November 17-19, 2014, Proceedings, LNCS,8858,58-77 Programming Languages and Systems 12th Asian Symposium, APLAS 2014, Singapore, Singapore, November 17-19, 2014, Proceedings, LNCS,8858,58-77 Programming Languages and Systems 12th Asian Symposium, APLAS 2014, Singapore, Singapore, November 17-19, 2014, Proceedings, LNCS,8858,58-77 2014/11 英語 研究論文(国際会議プロシーディングス) 公開
赤崎 拓未,蓮尾 一郎,末永 幸平 赤崎 拓未,蓮尾 一郎,末永 幸平 Takumi Akazaki, Ichiro Hasuo, and Kohei Suenaga Input Synthesis for Sampled Data Systems by Program Logic Input Synthesis for Sampled Data Systems by Program Logic Input Synthesis for Sampled Data Systems by Program Logic Proc. of the 4th Workshop on Hybrid Autonomous Systems (HAS 2014),22-39 Proc. of the 4th Workshop on Hybrid Autonomous Systems (HAS 2014),22-39 Proc. of the 4th Workshop on Hybrid Autonomous Systems (HAS 2014),22-39 2014 英語 研究論文(国際会議プロシーディングス) 公開
Tatsuya Sonobe,Kohei Suenaga,Atsushi Igarashi Tatsuya Sonobe,Kohei Suenaga,Atsushi Igarashi Tatsuya Sonobe,Kohei Suenaga,Atsushi Igarashi Automatic Memory Management Based on Program Transformation Using Ownership. Automatic Memory Management Based on Program Transformation Using Ownership. Automatic Memory Management Based on Program Transformation Using Ownership. Programming Languages and Systems - 12th Asian Symposium, APLAS 2014, Singapore, November 17-19, 2014, Proceedings,58-77 Programming Languages and Systems - 12th Asian Symposium, APLAS 2014, Singapore, November 17-19, 2014, Proceedings,58-77 Programming Languages and Systems - 12th Asian Symposium, APLAS 2014, Singapore, November 17-19, 2014, Proceedings,58-77 2014 公開
K. Suenaga; H. Sekine; I. Hasuo K. Suenaga; H. Sekine; I. Hasuo K. Suenaga; H. Sekine; I. Hasuo Hyperstream processing systems: Nonstandard modeling of continuous-time signals Hyperstream processing systems: Nonstandard modeling of continuous-time signals Hyperstream processing systems: Nonstandard modeling of continuous-time signals Conference Record of the Annual ACM Symposium on Principles of Programming Languages,417-430 Conference Record of the Annual ACM Symposium on Principles of Programming Languages,417-430 Conference Record of the Annual ACM Symposium on Principles of Programming Languages,417-430 2013 英語 公開
K. Suenaga; R. Fukuda; A. Igarashi K. Suenaga; R. Fukuda; A. Igarashi K. Suenaga; R. Fukuda; A. Igarashi Type-based safe resource deallocation for shared-memory concurrency Type-based safe resource deallocation for shared-memory concurrency Type-based safe resource deallocation for shared-memory concurrency Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA,1-20 Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA,1-20 Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA,1-20 2012 英語 公開
I. Hasuo; K. Suenaga I. Hasuo; K. Suenaga I. Hasuo; K. Suenaga Exercises in nonstandard static analysis of hybrid systems Exercises in nonstandard static analysis of hybrid systems Exercises in nonstandard static analysis of hybrid systems Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics),7358,462-478 Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics),7358,462-478 Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics),7358,462-478 2012 英語 公開
K. Suenaga; I. Hasuo K. Suenaga; I. Hasuo K. Suenaga; I. Hasuo Programming with infinitesimals: A While-language for hybrid system modeling Programming with infinitesimals: A While-language for hybrid system modeling Programming with infinitesimals: A While-language for hybrid system modeling Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics),6756,392-403 Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics),6756,392-403 Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics),6756,392-403 2011 英語 公開
Ryosuke Sato,Kohei Suenaga,Naoki Kobayashi 0001 Ryosuke Sato,Kohei Suenaga,Naoki Kobayashi 0001 Ryosuke Sato,Kohei Suenaga,Naoki Kobayashi 0001 Ordered Types for Stream Processing of Tree-Structured Data. Ordered Types for Stream Processing of Tree-Structured Data. Ordered Types for Stream Processing of Tree-Structured Data. JIP,19,74-87 JIP,19,74-87 JIP,19,74-87 2011 公開
佐藤 亮介, 末永 幸平, 小林 直樹 佐藤 亮介, 末永 幸平, 小林 直樹 Sato Ryosuke, Suenaga Kohei, Kobayashi Naoki RA-010 Ordered Types for Stream Processing of Tree-Structured Data RA-010 Ordered Types for Stream Processing of Tree-Structured Data RA-010 Ordered Types for Stream Processing of Tree-Structured Data 情報科学技術フォーラム講演論文集,8,1,65-72 情報科学技術フォーラム講演論文集,8,1,65-72 情報科学技術フォーラム講演論文集,8,1,65-72 2009/08/20 英語 公開
K. Suenaga; N. Kobayashi K. Suenaga; N. Kobayashi K. Suenaga; N. Kobayashi Fractional ownerships for safe memory deallocation Fractional ownerships for safe memory deallocation Fractional ownerships for safe memory deallocation Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics),5904,128-143 Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics),5904,128-143 Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics),5904,128-143 2009 英語 公開
飯村 枝里, 小林 直樹, 末永 幸平 飯村 枝里, 小林 直樹, 末永 幸平 飯村 枝里, 小林 直樹, 末永 幸平 型エラースライシングによるデッドロックの原因特定 型エラースライシングによるデッドロックの原因特定 Identifying Deadlock Errors by Type Error Slicing 情報処理学会論文誌プログラミング(PRO),1,2,71-84 情報処理学会論文誌プログラミング(PRO),1,2,71-84 情報処理学会論文誌プログラミング(PRO),1,2,71-84 2008/09/26 日本語 公開
K. Kodama; K. Suenaga; N. Kobayashi K. Kodama; K. Suenaga; N. Kobayashi K. Kodama; K. Suenaga; N. Kobayashi Translation of tree-processing programs into stream-processing programs based on ordered linear type Translation of tree-processing programs into stream-processing programs based on ordered linear type Translation of tree-processing programs into stream-processing programs based on ordered linear type Journal of Functional Programming,18,3,333-371 Journal of Functional Programming,18,3,333-371 Journal of Functional Programming,18,3,333-371 2008 英語 公開
Kohei Suenaga Kohei Suenaga Kohei Suenaga Type-Based Deadlock-Freedom Verification for Non-Block-Structured Lock Primitives and Mutable References. Type-Based Deadlock-Freedom Verification for Non-Block-Structured Lock Primitives and Mutable References. Type-Based Deadlock-Freedom Verification for Non-Block-Structured Lock Primitives and Mutable References. Programming Languages and Systems, 6th Asian Symposium, APLAS 2008, Bangalore, India, December 9-11, 2008. Proceedings,155-170 Programming Languages and Systems, 6th Asian Symposium, APLAS 2008, Bangalore, India, December 9-11, 2008. Proceedings,155-170 Programming Languages and Systems, 6th Asian Symposium, APLAS 2008, Bangalore, India, December 9-11, 2008. Proceedings,155-170 2008 公開
Kohei Suenaga,Naoki Kobayashi 0001 Kohei Suenaga,Naoki Kobayashi 0001 Kohei Suenaga,Naoki Kobayashi 0001 Type-Based Analysis of Deadlock for a Concurrent Calculus with Interrupts. Type-Based Analysis of Deadlock for a Concurrent Calculus with Interrupts. Type-Based Analysis of Deadlock for a Concurrent Calculus with Interrupts. 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 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 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 Naoki Kobayashi 0001,Kohei Suenaga,Lucian Wischik Naoki Kobayashi 0001,Kohei Suenaga,Lucian Wischik Resource Usage Analysis for the p-Calculus. Resource Usage Analysis for the p-Calculus. Resource Usage Analysis for the p-Calculus. Logical Methods in Computer Science,2,3 Logical Methods in Computer Science,2,3 Logical Methods in Computer Science,2,3 2006 公開
Naoki Kobayashi 0001,Kohei Suenaga,Lucian Wischik Naoki Kobayashi 0001,Kohei Suenaga,Lucian Wischik Naoki Kobayashi 0001,Kohei Suenaga,Lucian Wischik Resource Usage Analysis for the pi-Calculus. Resource Usage Analysis for the pi-Calculus. Resource Usage Analysis for the pi-Calculus. Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings,298-312 Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings,298-312 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 Naoki Kobayashi 0001,Kohei Suenaga,Lucian Wischik Naoki Kobayashi 0001,Kohei Suenaga,Lucian Wischik Resource Usage Analysis for the Pi-Calculus Resource Usage Analysis for the Pi-Calculus Resource Usage Analysis for the Pi-Calculus CoRR,abs/cs/0608035 CoRR,abs/cs/0608035 CoRR,abs/cs/0608035 2006 公開
Kohei Suenaga,Naoki Kobayashi 0001,Akinori Yonezawa Kohei Suenaga,Naoki Kobayashi 0001,Akinori Yonezawa Kohei Suenaga,Naoki Kobayashi 0001,Akinori Yonezawa Extension of Type-Based Approach to Generation of Stream-Processing Programs by Automatic Insertion of Buffering Primitives. Extension of Type-Based Approach to Generation of Stream-Processing Programs by Automatic Insertion of Buffering Primitives. Extension of Type-Based Approach to Generation of Stream-Processing Programs by Automatic Insertion of Buffering Primitives. Logic Based Program Synthesis and Transformation, 15th International Symposium, LOPSTR 2005, London, UK, September 7-9, 2005, Revised Selected Papers,3901,98-114 Logic Based Program Synthesis and Transformation, 15th International Symposium, LOPSTR 2005, London, UK, September 7-9, 2005, Revised Selected Papers,3901,98-114 Logic Based Program Synthesis and Transformation, 15th International Symposium, LOPSTR 2005, London, UK, September 7-9, 2005, Revised Selected Papers,3901,98-114 2005 公開
Koichi Kodama,Kohei Suenaga,Naoki Kobayashi 0001 Koichi Kodama,Kohei Suenaga,Naoki Kobayashi 0001 Koichi Kodama,Kohei Suenaga,Naoki Kobayashi 0001 Translation of Tree-Processing Programs into Stream-Processing Programs Based on Ordered Linear Type. Translation of Tree-Processing Programs into Stream-Processing Programs Based on Ordered Linear Type. Translation of Tree-Processing Programs into Stream-Processing Programs Based on Ordered Linear Type. Programming Languages and Systems: Second Asian Symposium, APLAS 2004, Taipei, Taiwan, November 4-6, 2004. Proceedings,41-56 Programming Languages and Systems: Second Asian Symposium, APLAS 2004, Taipei, Taiwan, November 4-6, 2004. Proceedings,41-56 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 Kohei Suenaga,Yutaka Oiwa,Eijiro Sumii,Akinori Yonezawa Kohei Suenaga,Yutaka Oiwa,Eijiro Sumii,Akinori Yonezawa The Interface Definition Language for Fail-Safe C. The Interface Definition Language for Fail-Safe C. The Interface Definition Language for Fail-Safe C. Software Security - Theories and Systems, Second Mext-NSF-JSPS International Symposium, ISSS 2003, Tokyo, Japan, November 4-6, 2003, Revised Papers,192-208 Software Security - Theories and Systems, Second Mext-NSF-JSPS International Symposium, ISSS 2003, Tokyo, Japan, November 4-6, 2003, Revised Papers,192-208 Software Security - Theories and Systems, Second Mext-NSF-JSPS International Symposium, ISSS 2003, Tokyo, Japan, November 4-6, 2003, Revised Papers,192-208 2003 公開
蓮尾 一郎,末永 幸平 蓮尾 一郎,末永 幸平 CPSの形式検証——超準解析によるアプローチ CPSの形式検証——超準解析によるアプローチ 計測と制御,53,12,1-6 計測と制御,53,12,1-6 ,53,12,1-6 日本語 研究論文(学術雑誌) 公開

  • <<
  • >>
  • 表示
タイトル言語:
講演・口頭発表等
タイトル タイトル(日本語) タイトル(英語) 会議名 会議名(日本語) 会議名(英語) 主催者 主催者(日本語) 主催者(英語) 開催年月日 記述言語 会議種別 公開
ニューラルネットワークによるフォトニック結晶格子点構造の3次元モデリングの検討 ニューラルネットワークによるフォトニック結晶格子点構造の3次元モデリングの検討 第65回応用物理学会春季学術講演会 第65回応用物理学会春季学術講演会 2018/03/20 日本語 ポスター発表 公開
Towards Proof Synthesis by Neural Machine Translation Towards Proof Synthesis by Neural Machine Translation Towards Proof Synthesis by Neural Machine Translation Off the Beaten Track 2018 (OBT 2018) Off the Beaten Track 2018 (OBT 2018) Off the Beaten Track 2018 (OBT 2018) 2018/01/13 英語 口頭発表(一般) 公開
A Guess-and-Assume Approach to Loop Fusion for Program Verification A Guess-and-Assume Approach to Loop Fusion for Program Verification A Guess-and-Assume Approach to Loop Fusion for Program Verification PEPM 2018 PEPM 2018 PEPM 2018 2018/01/08 英語 口頭発表(一般) 公開
A Guess-and-Assume Approach to Loop Fusion for Program Verification A Guess-and-Assume Approach to Loop Fusion for Program Verification A Guess-and-Assume Approach to Loop Fusion for Program Verification PEPM 2018 PEPM 2018 PEPM 2018 2018/01/07 英語 ポスター発表 公開
超準プログラミング言語を用いたハイブリッドシステムのモデリングと検証[招待あり] 超準プログラミング言語を用いたハイブリッドシステムのモデリングと検証 [招待あり] 第9回 暗号及び情報セキュリティと数学の相関ワークショップ (CRISMATH 2017) 第9回 暗号及び情報セキュリティと数学の相関ワークショップ (CRISMATH 2017) 2017/12/22 日本語 口頭発表(招待・特別) 公開
Sharper and Simpler Nonlinear Interpolants for Program Verification Sharper and Simpler Nonlinear Interpolants for Program Verification Sharper and Simpler Nonlinear Interpolants for Program Verification APLAS 2017 APLAS 2017 APLAS 2017 2017/11/27 英語 口頭発表(一般) 公開
A Nonstandard Functional Programming Language A Nonstandard Functional Programming Language A Nonstandard Functional Programming Language APLAS 2017 APLAS 2017 APLAS 2017 2017/11/27 英語 口頭発表(一般) 公開
Efficient Online Timed Pattern Matching by Automata-Based Skipping Efficient Online Timed Pattern Matching by Automata-Based Skipping Efficient Online Timed Pattern Matching by Automata-Based Skipping 15th International Conference on Formal Modelling and Analysis of Timed Systems 15th International Conference on Formal Modelling and Analysis of Timed Systems 15th International Conference on Formal Modelling and Analysis of Timed Systems 2017/09/05 英語 口頭発表(一般) 公開
Sharper and Simpler Nonlinear Interpolants for Program Verification Sharper and Simpler Nonlinear Interpolants for Program Verification Sharper and Simpler Nonlinear Interpolants for Program Verification Workshop on Formal Approaches to Explainable VERification (FEVER 2017) Workshop on Formal Approaches to Explainable VERification (FEVER 2017) Workshop on Formal Approaches to Explainable VERification (FEVER 2017) 2017/07/23 英語 口頭発表(一般) 公開
Generalized Homogeneous Polynomials for Efficient Template-Based Nonlinear Invariant Synthesis Generalized Homogeneous Polynomials for Efficient Template-Based Nonlinear Invariant Synthesis 第19回プログラミングおよびプログラミング言語ワークショップ(PPL2017) 第19回プログラミングおよびプログラミング言語ワークショップ(PPL2017) 2017/03/08 口頭発表(一般) 公開
無限状態システムのHFLモデル検査のための型に基づく手法 無限状態システムのHFLモデル検査のための型に基づく手法 第19回プログラミングおよびプログラミング言語ワークショップ(PPL2017) 第19回プログラミングおよびプログラミング言語ワークショップ(PPL2017) 2017/03/08 日本語 ポスター発表 公開
深層学習によるプログラム生成の高速化 深層学習によるプログラム生成の高速化 第19回プログラミングおよびプログラミング言語ワークショップ(PPL2017) 第19回プログラミングおよびプログラミング言語ワークショップ(PPL2017) 2017/03/08 日本語 ポスター発表 公開
超準関数型プログラミング言語NSF 超準関数型プログラミング言語NSF 第19回プログラミングおよびプログラミング言語ワークショップ(PPL2017) 第19回プログラミングおよびプログラミング言語ワークショップ(PPL2017) 2017/03/08 日本語 ポスター発表 公開
そのプログラム、バグってないですか?:数学を使ってバグを見つけるための形式検証手法[招待あり] そのプログラム、バグってないですか?:数学を使ってバグを見つけるための形式検証手法 [招待あり] 2016年度情報処理学会関西支部定期講演会「IoT の周辺技術」 2016年度情報処理学会関西支部定期講演会「IoT の周辺技術」 2016/12/21 公開講演、セミナー、チュートリアル、講習、講義 公開
超準解析を用いたハイブリッドシステム検証手法[招待あり] 超準解析を用いたハイブリッドシステム検証手法 [招待あり] 統計数理解析研究所シンポジウム --- 工学と現代数学の接点を求めて 統計数理解析研究所シンポジウム --- 工学と現代数学の接点を求めて 2016/12/20 シンポジウム・ワークショップパネル(指名) 公開
Generalized Homogeneous Polynomials for Efficient Template-Based Nonlinear Invariant Synthesis Generalized Homogeneous Polynomials for Efficient Template-Based Nonlinear Invariant Synthesis Generalized Homogeneous Polynomials for Efficient Template-Based Nonlinear Invariant Synthesis SAS 2016 SAS 2016 SAS 2016 2016/09/08 英語 口頭発表(一般) 公開
An Extended Behavioral Type System for Memory-Leak Freedom An Extended Behavioral Type System for Memory-Leak Freedom An Extended Behavioral Type System for Memory-Leak Freedom 日本ソフトウェア科学会 第33回大会講演論文集 日本ソフトウェア科学会 第33回大会講演論文集 2016/09/07 英語 口頭発表(一般) 公開
ソフトウェアのための自動形式検証ツール ソフトウェアのための自動形式検証ツール ET/IoT 総合技術展 関西(ETWest 2016) ET/IoT 総合技術展 関西(ETWest 2016) 2016/07/07 日本語 ポスター発表 公開
そのプログラム、バグってないですか? ― 数学を使ってバグを見つける[招待あり] そのプログラム、バグってないですか? ― 数学を使ってバグを見つける [招待あり] JST 京都大学新技術説明会 JST 京都大学新技術説明会 2016/05/24 日本語 公開講演、セミナー、チュートリアル、講習、講義 公開
Formal verification of software, continuous, and hybrid systems -- Or: How do we verify our program is correct? Formal verification of software, continuous, and hybrid systems -- Or: How do we verify our program is correct? Formal verification of software, continuous, and hybrid systems -- Or: How do we verify our program is correct? Machine Learning Summer School 2015 Machine Learning Summer School 2015 Machine Learning Summer School 2015 2015/08/27 英語 公開講演、セミナー、チュートリアル、講習、講義 公開
Nonstandard Analysis Meets Programming Language Theory[招待あり] Nonstandard Analysis Meets Programming Language Theory [招待あり] Nonstandard Analysis Meets Programming Language Theory [招待あり] Twelfth International Conference on Computability and Complexity in Analysis Twelfth International Conference on Computability and Complexity in Analysis Twelfth International Conference on Computability and Complexity in Analysis 2015/07/13 英語 口頭発表(招待・特別) 公開
Automatic Synthesis of Combiners in the MapReduce Framework Automatic Synthesis of Combiners in the MapReduce Framework Automatic Synthesis of Combiners in the MapReduce Framework 24th International Symposium on Logic-Based Program Synthesis and Transformation 24th International Symposium on Logic-Based Program Synthesis and Transformation 24th International Symposium on Logic-Based Program Synthesis and Transformation 2014/09/09 英語 口頭発表(一般) 公開
Type-Based Safe Resource Deallocation for Shared-Memory Concurrency[招待あり] Type-Based Safe Resource Deallocation for Shared-Memory Concurrency [招待あり] 日本ソフトウェア科学会第30回大会特別招待講演 日本ソフトウェア科学会第30回大会特別招待講演 2013/09/12 日本語 口頭発表(招待・特別) 公開
形式検証手法は無限小プログラミングを使えばハイブリッドシステムにもそのまま使える[招待あり] 形式検証手法は無限小プログラミングを使えばハイブリッドシステムにもそのまま使える [招待あり] 日本ソフトウェア科学会第30回大会Future Technology Design (FTD) 2013 日本ソフトウェア科学会第30回大会Future Technology Design (FTD) 2013 2013/09/11 日本語 口頭発表(招待・特別) 公開
Simulink blocks as stream processing ─ An approach from nonstandard analysis (Preliminary Report) Simulink blocks as stream processing ─ An approach from nonstandard analysis (Preliminary Report) Simulink blocks as stream processing ─ An approach from nonstandard analysis (Preliminary Report) Fifth International Workshop on Numerical Software Verification (NSV 2012) Fifth International Workshop on Numerical Software Verification (NSV 2012) Fifth International Workshop on Numerical Software Verification (NSV 2012) 2012/07/07 英語 口頭発表(一般) 公開

  • <<
  • >>
  • 表示
タイトル言語:
特許
発明者 発明者(日本語) 発明者(英語) 発明の名称 発明の名称(日本語) 発明の名称(英語) 審査の段階 番号 年月 公開
末永 幸平, 蓮尾 一郎 末永 幸平, 蓮尾 一郎 ハイブリッドシステムの検証方法、検証装置、及び検証コンピュータプログラム、並びに、ハイブリッドシステムのモデル変換方法、変換装置、及び変換コンピュータプログラム ハイブリッドシステムの検証方法、検証装置、及び検証コンピュータプログラム、並びに、ハイブリッドシステムのモデル変換方法、変換装置、及び変換コンピュータプログラム 特許登録 特許第5843230号 2015/11/27 公開
末永 幸平,蓮尾 一郎 末永 幸平,蓮尾 一郎 ハイブリッドシステムの検証方法、検証装置、及び検証コンピュータプログラム、並びに、ハイブリ ッドシステムのモデル変換方法、変換装置、及び変換コンピュータプログラム ハイブリッドシステムの検証方法、検証装置、及び検証コンピュータプログラム、並びに、ハイブリ ッドシステムのモデル変換方法、変換装置、及び変換コンピュータプログラム 特許登録 特許5843230 2015/11/27 公開
中村 宏明,宮下 尚,末永 幸平 中村 宏明,宮下 尚,末永 幸平 Hiroaki Nakamura, Hisashi Miyashita, and Kohei Suenaga 情報管理システム、方法及びプログラム 情報管理システム、方法及びプログラム INFORMATION MANAGEMENT SYSTEM, METHOD AND PROGRAM 特許登録 特許第5431261号 2013/12/13 公開
末永 幸平, 今西 諒文, 五十嵐 淳 末永 幸平, 今西 諒文, 五十嵐 淳 プログラム検証装置、プログラム検証方法、プログラム検証のためのコンピュータプログラム、プログラム変換器、プログラム変換方法、プログラム変換のためのコンピュータプログラム、プログラム製造方法、及び検証用プログラム プログラム検証装置、プログラム検証方法、プログラム検証のためのコンピュータプログラム、プログラム変換器、プログラム変換方法、プログラム変換のためのコンピュータプログラム、プログラム製造方法、及び検証用プログラム 特許出願 特願2017-246154 2017/12/22 公開
蓮尾 一郎,奥殿 貴仁,木戸 肩吾,末永 幸平,小島 健介,西田 雄気 蓮尾 一郎,奥殿 貴仁,木戸 肩吾,末永 幸平,小島 健介,西田 雄気 自動証明装置、及びプログラム 自動証明装置、及びプログラム 特許出願 特願2017-137949 2017/07/14 公開
樹下稔,小島健介,末永幸平 樹下稔,小島健介,末永幸平 不変条件生成装置、コンピュータプログラム、不変条件生成方法、プログラムコード製造方法 不変条件生成装置、コンピュータプログラム、不変条件生成方法、プログラムコード製造方法 特許出願 PCT/JP2017/003295 2017/01/31 公開
末永 幸平,樹下 稔,小島 健介 末永 幸平,樹下 稔,小島 健介 不変条件生成装置、コンピュータプログラム、不変条件生成方法、プログラムコード製造方法 不変条件生成装置、コンピュータプログラム、不変条件生成方法、プログラムコード製造方法 特許公開 特開2017-138679 2017/08/10 公開
末永 幸平,樹下 稔,小島 健介 末永 幸平,樹下 稔,小島 健介 不変条件生成装置、コンピュータプログラム、不変条件生成方法、プログラムコード製造方法 不変条件生成装置、コンピュータプログラム、不変条件生成方法、プログラムコード製造方法 特許公開 特開2017-138677 2017/08/10 公開
赤崎 拓未,蓮尾 一郎,末永 幸平 赤崎 拓未,蓮尾 一郎,末永 幸平 制御入力値生成装置,制御入力値生成方法,および,プログラム 制御入力値生成装置,制御入力値生成方法,および,プログラム 特許出願 特願2014-72623 2014/03/31 公開
蓮尾 一郎, 赤崎 拓未, 末永 幸平 蓮尾 一郎, 赤崎 拓未, 末永 幸平 制御入力値生成装置、制御入力値生成方法、および、プログラム 制御入力値生成装置、制御入力値生成方法、および、プログラム 特許公開 特開2015-194917 2015/11/05 公開
中村 宏明, 宮下 尚, 末永 幸平 中村 宏明, 宮下 尚, 末永 幸平 情報管理システム、方法及びプログラム 情報管理システム、方法及びプログラム 特許公開 特開2012-027685 2012/02/09 公開
宮下尚,中村宏明,末永幸平 宮下尚,中村宏明,末永幸平 Hisashi Miyashita, Hiroaki Nakamura, Kohei Suenaga Information management system, method and program Information management system, method and program Information management system, method and program 特許登録 特許8766980 公開

  • <<
  • >>
  • 表示
タイトル言語:
外部資金:競争的資金・科学研究費補助金
種別 代表/分担 テーマ(日本語) テーマ(英語) 期間
特別研究員奨励費 並行プログラムのための型理論に基づく利便性の高い静的検証手法 2011〜2011
研究活動スタート支援 代表 無限小プログラミングによるハイブリッドシステムの形式検証手法 2012〜2013
若手研究(B) 代表 無限小プログラミングによるハイブリッドシステムの形式検証手法 2013〜2015
若手研究(B) 代表 無限小プログラミングによるハイブリッドシステムの形式検証手法 (平成26年度分) 2014/04/01〜2015/03/31
若手研究(B) 代表 無限小プログラミングによるハイブリッドシステムの形式検証手法 (平成27年度分) 2015/04/01〜2016/03/31
JST さきがけ 代表 ハイブリッドシステムのための超準プログラミング言語理論を用いた形式手法 Formal methods for hybrid systems based on the theory of nonstandard programming languages 2015/10/01〜2019/03/31
担当科目
講義名(日本語) 講義名(英語) 開講期 学部/研究科 年度
計算機科学実験及演習4 Computer Science Laboratory and Exercise 4 後期 工学部 2013/04〜2014/03
計算機科学実験及演習1 Computer Science Laboratory and Exercise 1 前期 工学部 2014/04〜2015/03
計算機科学実験及演習4 Computer Science Laboratory and Exercise 4 後期 工学部 2014/04〜2015/03
コンパイラ Compilers 後期 工学部 2014/04〜2015/03
プログラム意味論 Formal Semantics of Computer Programs 前期 情報学研究科 2014/04〜2015/03
並列分散システム論 Parallel and Distributed Systems 後期 情報学研究科 2014/04〜2015/03
コンピュータ工学特別セミナー Seminar on Computer Engineering, Advanced 通年 情報学研究科 2014/04〜2015/03
通信情報システム特別研究2 Advanced Study in Communications and Computer Engineering II 後期前期 情報学研究科 2014/04〜2015/03
通信情報システム特別研究1 Advanced Study in Communications and Computer Engineering I 通年 情報学研究科 2014/04〜2015/03
Advanced Study in CCE I Advanced Study in Communications and Computer Engineering I 通年 情報学研究科 2015/04〜2016/03
Advanced Study in CCE II Advanced Study in Communications and Computer Engineering II 通年 情報学研究科 2015/04〜2016/03
コンパイラ Compilers 後期 工学部 2015/04〜2016/03
並列分散システム論 Parallel and Distributed Systems 後期 情報学研究科 2015/04〜2016/03
ゲーム制作で学ぶ関数型プログラミング言語 Learning a functional programming language by game creating 前期 全学共通科目 2015/04〜2016/03
コンピュータ工学特別セミナー Seminar on Computer Engineering, Advanced 通年 情報学研究科 2015/04〜2016/03
プログラム意味論 Formal Semantics of Computer Programs 前期 情報学研究科 2015/04〜2016/03
計算機科学実験及演習1 Computer Science Laboratory and Exercise 1 前期 工学部 2015/04〜2016/03
計算機科学実験及演習2 Computer Science Laboratory and Exercise 2 後期 工学部 2015/04〜2016/03
計算機科学実験及演習3 Computer Science Laboratory and Exercise 3 前期 工学部 2015/04〜2016/03
計算機科学実験及演習4 Computer Science Laboratory and Exercise 4 後期 工学部 2015/04〜2016/03
通信情報システム特別研究2 Advanced Study in Communications and Computer Engineering II 後期集中 情報学研究科 2015/04〜2016/03
通信情報システム特別研究2 Advanced Study in Communications and Computer Engineering II 通年 情報学研究科 2015/04〜2016/03
通信情報システム特別研究1 Advanced Study in Communications and Computer Engineering I 通年 情報学研究科 2015/04〜2016/03
Advanced Study in CCE I Advanced Study in Communications and Computer Engineering I 通年 情報学研究科 2016/04〜2017/03
Advanced Study in CCE II Advanced Study in Communications and Computer Engineering II 通年 情報学研究科 2016/04〜2017/03
ILASセミナー ILAS Seminar 前期 全学共通科目 2016/04〜2017/03
Parallel and Distributed Systems Parallel and Distributed Systems 後期 情報学研究科 2016/04〜2017/03
コンピュータ工学特別セミナー Seminar on Computer Engineering, Advanced 通年 情報学研究科 2016/04〜2017/03
プログラム意味論 Formal Semantics of Computer Programs 前期 情報学研究科 2016/04〜2017/03
計算機科学実験及演習4 Computer Science Laboratory and Exercise 4 後期 工学部 2016/04〜2017/03
計算機科学のための数学演習 Mathematics in Practice for Computer Science 前期 工学部 2016/04〜2017/03
通信情報システム特別研究2 Advanced Study in Communications and Computer Engineering II 前期集中 情報学研究科 2016/04〜2017/03
通信情報システム特別研究2 Advanced Study in Communications and Computer Engineering II 通年 情報学研究科 2016/04〜2017/03
通信情報システム特別研究1 Advanced Study in Communications and Computer Engineering I 通年 情報学研究科 2016/04〜2017/03
Advanced Study in CCE I Advanced Study in Communications and Computer Engineering I 通年 情報学研究科 2017/04〜2018/03
Advanced Study in CCE II Advanced Study in Communications and Computer Engineering II 通年 情報学研究科 2017/04〜2018/03
Parallel and Distributed Systems Parallel and Distributed Systems 後期 情報学研究科 2017/04〜2018/03
コンピュータ工学特別セミナー Seminar on Computer Engineering, Advanced 通年 情報学研究科 2017/04〜2018/03
プログラム意味論 Formal Semantics of Computer Programs 前期 情報学研究科 2017/04〜2018/03
プログラミング言語処理系 Implementation of Programming Languages 前期 工学部 2017/04〜2018/03
計算機科学実験及演習3 Computer Science Laboratory and Exercise 3 前期 工学部 2017/04〜2018/03
計算機科学のための数学演習 Mathematics in Practice for Computer Science 前期 工学部 2017/04〜2018/03
通信情報システム特別研究2 Advanced Study in Communications and Computer Engineering II 前期集中 情報学研究科 2017/04〜2018/03
通信情報システム特別研究2 Advanced Study in Communications and Computer Engineering II 通年 情報学研究科 2017/04〜2018/03
通信情報システム特別研究1 Advanced Study in Communications and Computer Engineering I 通年 情報学研究科 2017/04〜2018/03
Parallel and Distributed Systems Parallel and Distributed Systems 後期 情報学研究科 2018/04〜2019/03
情報と職業 Information and Business 前期 工学部 2018/04〜2019/03
プログラム意味論 Formal Semantics of Computer Programs 前期 情報学研究科 2018/04〜2019/03
プログラミング言語処理系 Implementation of Programming Languages 前期 工学部 2018/04〜2019/03
計算機科学実験及演習3 Computer Science Laboratory and Exercise 3 前期 工学部 2018/04〜2019/03
計算機科学のための数学演習 Mathematics in Practice for Computer Science 前期 工学部 2018/04〜2019/03

  • <<
  • >>
  • 表示
部局運営(役職等)
役職名 期間
情報セキュリティ作業委員会委員 2015/04/01〜2017/03/31
計算機小委員会委員 2015/04/01〜2017/03/31
ハラスメント窓口相談員 2015/04/01〜2016/03/31
図書WG委員 2016/04/01〜2017/03/31
情報セキュリティ作業委員会委員 2017/04/01〜2018/03/31
計算機小委員会委員 2017/04/01〜2018/03/31
図書WG委員 2017/04/01〜2018/03/31
情報セキュリティ委員会委員(情報セキュリティ副技術責任者) 2018/04/01〜2019/03/31
情報セキュリティ作業委員会委員 2018/04/01〜2019/03/31
計算機小委員会委員 2018/04/01〜2019/03/31