末永 幸平

Last Update: 2021/06/24 14:36:23

Print

Name(Kanji/Kana/Abecedarium Latinum)
末永 幸平/スエナガ コウヘイ/Suenaga, Kohei
Primary Affiliation(Org1/Job title)
Graduate School of Informatics/Associate Professor
Faculty
Org1 Job title
工学部
Academic Degree
Field(Japanese) Field(English) University(Japanese) University(English) Method
修士(情報理工学) Master in Information Science and Technology 東京大学 The University of Tokyo
博士(情報理工学) Ph.D. in Information Science and Technology 東京大学 The University of Tokyo
Academic Resume (Graduate Schools)
University(Japanese) University(English) Faculty(Japanese) Faculty(English) Major(Japanese) Major(English) Completion Status
東京大学 The University of Tokyo 大学院情報理工学系研究科コンピュータ科学専攻修士課程 修了
東京大学 The University of Tokyo 大学院情報理工学系研究科コンピュータ科学専攻博士課程 修了
Academic Resume (Undergraduate School/Majors)
University(Japanese) University(English) Faculty(Japanese) Faculty(English) Major(s)(Japanese) Major(s)(English) Completion Status
東京大学 The University of Tokyo 理学部情報科学科 卒業
東京大学 The University of Tokyo 教養学部理科一類
High School
Highschool Kana
宮崎県立宮崎西高等学校 みやざきけんりつみやざきにしこうとうがっこう
Work Experience
Period Organization(Japanese) Organization(English) Job title(Japanese) Job title(English)
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
Language of Instruction
Language(japanese) Language(english) Code
英語 English eng
ポルトガル語 Portuguese por
ORCID ID
https://orcid.org/0000-0002-7466-8789
researchmap URL
https://researchmap.jp/ksuenaga
Research Topics
(Japanese)
形式検証手法
(English)
Formal verification
Overview of the research
(Japanese)
さまざまなシステムのための形式検証手法を研究しています.形式検証とは,数学を用いてシステムのバグを発見したり,システムにバグが存在しないことを証明したりするための手法です.もともとハードウェアを検査するための手法として提案された手法ですが,コンピュータが社会の様々なところで用いられるに従って,ソフトウェアを検証するための手法としても広く用いられるようになっています.また近年では,伝統的なソフトウェアに限らず,ハイブリッドシステム(プログラムと微分方程式との組み合わせで記述されるシステム)や機械学習システム等,検証が必要なシステムの種類が増えてきています. 末永はプログラミング言語理論に関する専門的知見をコアとして,この知見を様々なシステムに適用するための研究を行っています.最近はハイブリッドシステム,スマートコントラクト,機械学習システムの検証手法を研究しています.もちろん,普通のソフトウェアに適用可能な手法も研究しています.
(English)
My main research topic is on formal verification techniques for various types of systems. Formal verification is a methodology for detecting bugs in a system and proving the correctness of a system. It was originally a method for verifying the correctness of hardware; then, it has been widely applied to software verification as computers are widely used in the world. In addition to traditional software, our world is full of systems that need to be verified: To name a few, hybrid systems (that are described as a combination of programs and differential equations) and machine learning systems. My recent research topic is to apply techniques for software verification to these various systems. Recent research topics include formal verification of hybrid systems, smart contracts, machine learning systems, and software systems.
Fields of research (key words)
Key words(Japanese) Key words(English)
ソフトウェア software
ハイブリッドシステム hybrid systems
プログラム検証 program verification
形式手法 formal methods
プログラミング言語理論 theory of programming languages
機械学習 Machine learning
スマートコントラクト Smart contracts
Published Papers
Author Author(Japanese) Author(English) Title Title(Japanese) Title(English) Bibliography Bibliography(Japanese) Bibliography(English) Publication date Refereed paper Language Publishing type Disclose
Sota Sato, Ryotaro Banno, Jun Furuse, Kohei Suenaga, Atsushi Igarashi Sota Sato, Ryotaro Banno, Jun Furuse, Kohei Suenaga, Atsushi Igarashi Sota Sato, Ryotaro Banno, Jun Furuse, Kohei Suenaga, Atsushi Igarashi Verification of a Merkle Patricia Tree Library Using F. Verification of a Merkle Patricia Tree Library Using F. Verification of a Merkle Patricia Tree Library Using F. CoRR, abs/2106.04826 CoRR, abs/2106.04826 CoRR, abs/2106.04826 2021 Research paper(scientific journal) Disclose to all
Ichiro Hasuo, Yuichiro Oyabu, Clovis Eberhart, Kohei Suenaga, Kenta Cho 0002, Shin-ya Katsumata Ichiro Hasuo, Yuichiro Oyabu, Clovis Eberhart, Kohei Suenaga, Kenta Cho 0002, Shin-ya Katsumata Ichiro Hasuo, Yuichiro Oyabu, Clovis Eberhart, Kohei Suenaga, Kenta Cho 0002, Shin-ya Katsumata Control-Data Separation and Logical Condition Propagation for Efficient Inference on Probabilistic Programs. Control-Data Separation and Logical Condition Propagation for Efficient Inference on Probabilistic Programs. Control-Data Separation and Logical Condition Propagation for Efficient Inference on Probabilistic Programs. CoRR, abs/2101.01502 CoRR, abs/2101.01502 CoRR, abs/2101.01502 2021 Research paper(scientific journal) Disclose to all
Yuki Nishida 0001, Hiromasa Saito, Ran Chen, Akira Kawata, Jun Furuse, Kohei Suenaga, Atsushi Igarashi Yuki Nishida 0001, Hiromasa Saito, Ran Chen, Akira Kawata, Jun Furuse, Kohei Suenaga, Atsushi Igarashi Yuki Nishida 0001, Hiromasa Saito, Ran Chen, Akira Kawata, Jun Furuse, Kohei Suenaga, Atsushi Igarashi Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types. Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types. Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types. Proceedings of TACAS 2021, 262-280 Proceedings of TACAS 2021, 262-280 Proceedings of TACAS 2021, 262-280 2021 English Research paper(international conference proceedings) Disclose to all
齋藤 大聖, 西田 雄気, 五十嵐 淳, 末永 幸平 齋藤 大聖, 西田 雄気, 五十嵐 淳, 末永 幸平 スマートコントラクトのための Effectively Callback-Free 性の型に基づく静的検証 スマートコントラクトのための Effectively Callback-Free 性の型に基づく静的検証 PPL 2020 PPL 2020 2020/03 Refereed Japanese Research paper(research society, symposium, etc.) Disclose to all
佐藤 聡太, 古瀬 淳, 末永 幸平, 五十嵐 淳 佐藤 聡太, 古瀬 淳, 末永 幸平, 五十嵐 淳 F*を用いたMerkle Patricia Treeライブラリの形式検証 F*を用いたMerkle Patricia Treeライブラリの形式検証 PPL 2020 PPL 2020 2020/03 Refereed Japanese Research paper(research society, symposium, etc.) Disclose to all
Yuhki Hatakeyama, Hiroki Sakuma, Yoshinori Konishi, Kohei Suenaga Yuhki Hatakeyama, Hiroki Sakuma, Yoshinori Konishi, Kohei Suenaga Visualizing Color-Wise Saliency of Black-Box Image Classification Models. Visualizing Color-Wise Saliency of Black-Box Image Classification Models. Visualizing Color-Wise Saliency of Black-Box Image Classification Models. ACCV 2020, 189-205 ACCV 2020, 189-205 ACCV 2020, 189-205 2020 Research paper(international conference proceedings) Disclose to all
John Toman, Ren Siqi, Kohei Suenaga, Atsushi Igarashi, Naoki Kobayashi 0001 John Toman, Ren Siqi, Kohei Suenaga, Atsushi Igarashi, Naoki Kobayashi 0001 John Toman, Ren Siqi, Kohei Suenaga, Atsushi Igarashi, Naoki Kobayashi 0001 ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs. ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs. ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs. CoRR, abs/2002.07770 CoRR, abs/2002.07770 CoRR, abs/2002.07770 2020 Research paper(scientific journal) Disclose to all
Kohei Suenaga, Takuya Ishizawa Kohei Suenaga, Takuya Ishizawa Kohei Suenaga, Takuya Ishizawa Generalized Property-Directed Reachability for Hybrid Systems Generalized Property-Directed Reachability for Hybrid Systems Generalized Property-Directed Reachability for Hybrid Systems , 293-313 , 293-313 , 293-313 2020 Refereed Research paper(international conference proceedings) Disclose to all
Ruka Funaki, Yusuke Nagata, Kohei Suenaga, Shinsuke Mori Ruka Funaki, Yusuke Nagata, Kohei Suenaga, Shinsuke Mori Ruka Funaki, Yusuke Nagata, Kohei Suenaga, Shinsuke Mori A Contract Corpus for Recognizing Rights and Obligations. A Contract Corpus for Recognizing Rights and Obligations. A Contract Corpus for Recognizing Rights and Obligations. , 2045-2053 , 2045-2053 , 2045-2053 2020 Refereed Research paper(international conference proceedings) Disclose to all
John Toman, Ren Siqi, Kohei Suenaga, Atsushi Igarashi, Naoki Kobayashi John Toman, Ren Siqi, Kohei Suenaga, Atsushi Igarashi, Naoki Kobayashi John Toman, Ren Siqi, Kohei Suenaga, Atsushi Igarashi, Naoki Kobayashi ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs Programming Languages and Systems, 684-714 Programming Languages and Systems, 684-714 Programming Languages and Systems, 684-714 2020 Refereed Research paper(international conference proceedings) Disclose to all
Kohei Suenaga, Takuya Ishizawa Kohei Suenaga, Takuya Ishizawa Kohei Suenaga, Takuya Ishizawa Generalized Property-Directed Reachability for Hybrid Systems. Generalized Property-Directed Reachability for Hybrid Systems. Generalized Property-Directed Reachability for Hybrid Systems. CoRR, abs/1910.03784, 1-21 CoRR, abs/1910.03784, 1-21 CoRR, abs/1910.03784, 1-21 2019 Refereed English Research paper(scientific journal) Disclose to all
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 Theoretical Computer Science, 747, 33-47 Theoretical Computer Science, 747, 33-47 Theoretical Computer Science, 747, 33-47 2018 Refereed English Research paper(scientific journal) Disclose to all
Taro Sekiyama, Kohei Suenaga Taro Sekiyama, Kohei Suenaga Taro Sekiyama, Kohei Suenaga Automated Proof Synthesis for the Minimal Propositional Logic with Deep Neural Networks Automated Proof Synthesis for the Minimal Propositional Logic with Deep Neural Networks Automated Proof Synthesis for the Minimal Propositional Logic with Deep Neural Networks APLAS 2018, 309-328 APLAS 2018, 309-328 APLAS 2018, 309-328 2018 Refereed English Research paper(international conference proceedings) Disclose to all
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 Refereed English Research paper(international conference proceedings) Disclose to all
Masaki Waga, Ichiro Hasuo, Kohei Suenaga Masaki Waga, Ichiro Hasuo, Kohei Suenaga Masaki Waga, Ichiro Hasuo, Kohei Suenaga MONAA: A Tool for Timed Pattern Matching with Automata-Based Acceleration. MONAA: A Tool for Timed Pattern Matching with Automata-Based Acceleration. MONAA: A Tool for Timed Pattern Matching with Automata-Based Acceleration. CoRR, abs/1810.09351 CoRR, abs/1810.09351 CoRR, abs/1810.09351 2018 Refereed Research paper(scientific journal) Disclose to all
Taro Sekiyama, Kohei Suenaga Taro Sekiyama, Kohei Suenaga Taro Sekiyama, Kohei Suenaga Automated proof synthesis for propositional logic with deep neural networks. Automated proof synthesis for propositional logic with deep neural networks. Automated proof synthesis for propositional logic with deep neural networks. CoRR, abs/1805.11799 CoRR, abs/1805.11799 CoRR, abs/1805.11799 2018 Refereed Research paper(scientific journal) Disclose to all
Masaki Waga, Ichiro Hasuo, Kohei Suenaga Masaki Waga, Ichiro Hasuo, Kohei Suenaga Masaki Waga, Ichiro Hasuo, Kohei Suenaga MONAA: A Tool for Timed Pattern Matching with Automata-Based Acceleration. MONAA: A Tool for Timed Pattern Matching with Automata-Based Acceleration. MONAA: A Tool for Timed Pattern Matching with Automata-Based Acceleration. 3rd Workshop on Monitoring and Testing of Cyber-Physical Systems, MT@CPSWeek 2018, Porto, Portugal, April 10, 2018, 14-15 3rd Workshop on Monitoring and Testing of Cyber-Physical Systems, MT@CPSWeek 2018, Porto, Portugal, April 10, 2018, 14-15 3rd Workshop on Monitoring and Testing of Cyber-Physical Systems, MT@CPSWeek 2018, Porto, Portugal, April 10, 2018, 14-15 2018 Refereed Research paper(international conference proceedings) Disclose to all
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. Theor. Comput. Sci., 747, 33-47 Theor. Comput. Sci., 747, 33-47 Theor. Comput. Sci., 747, 33-47 2018 Refereed English Research paper(scientific journal) Disclose to all
末永 幸平 末永 幸平 末永 幸平 PLDI 2016 Report 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 Japanese Disclose to all
Takamasa Okudono, Yuki Nishida 0001, Kensuke Kojima, Kohei Suenaga, Kengo Kido, Ichiro Hasuo Takamasa Okudono, Yuki Nishida 0001, Kensuke Kojima, Kohei Suenaga, Kengo Kido, Ichiro Hasuo Takamasa Okudono, Yuki Nishida 0001, 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, 491-513 CoRR, abs/1709.00314, 491-513 CoRR, abs/1709.00314, 491-513 2017 Refereed English Research paper(scientific journal) Disclose to all
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, 491-513 CoRR, abs/1709.00314, 491-513 CoRR, abs/1709.00314, 491-513 2017 Refereed English Research paper(scientific journal) Disclose to all
Hirofumi Nakamura, Kensuke Kojima, Kohei Suenaga, Atsushi Igarashi Hirofumi Nakamura, Kensuke Kojima, Kohei Suenaga, Atsushi Igarashi Hirofumi Nakamura, Kensuke Kojima, Kohei Suenaga, Atsushi Igarashi A Nonstandard Functional Programming Language. A Nonstandard Functional Programming Language. A Nonstandard Functional Programming Language. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 10695, 514-533 Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 10695, 514-533 Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 10695, 514-533 2017 Refereed English Research paper(international conference proceedings) Disclose to all
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 Refereed Research paper(scientific journal) Disclose to all
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 Refereed Research paper(scientific journal) Disclose to all
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, 224-243 CoRR, abs/1706.09174, 224-243 CoRR, abs/1706.09174, 224-243 2017 Refereed English Research paper(scientific journal) Disclose to all
Qi Tan, Kohei Suenaga, Atsushi Igarashi Qi Tan, Kohei Suenaga, Atsushi Igarashi Qi Tan, Kohei Suenaga, Atsushi Igarashi 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 English Research paper(research society, symposium, etc.) Disclose to all
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, 278-299 CoRR, abs/1604.07201, 278-299 CoRR, abs/1604.07201, 278-299 2016 Refereed English Research paper(scientific journal) Disclose to all
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, (SAS 2016), 9837, 278-299 STATIC ANALYSIS, (SAS 2016), 9837, 278-299 STATIC ANALYSIS, (SAS 2016), 9837, 278-299 2016 Refereed English Research paper(international conference proceedings) Disclose to all
Takumi Akazaki, Ichiro Hasuo, Kohei Suenaga Takumi Akazaki, Ichiro Hasuo, Kohei Suenaga Takumi Akazaki, Ichiro Hasuo, 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 2015/01/24 Refereed English Disclose to all
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 Refereed Disclose to all
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, 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 Refereed English Research paper(international conference proceedings) Disclose to all
Minoru Kinoshita, Kohei Suenaga, Atsushi Igarashi Minoru Kinoshita, Kohei Suenaga, Atsushi Igarashi Minoru Kinoshita, Kohei Suenaga, Atsushi Igarashi Automatic Synthesis of Combiners in the MapReduce Framework: An Approach with Right Inverse Automatic Synthesis of Combiners in the MapReduce Framework: An Approach with Right Inverse Automatic Synthesis of Combiners in the MapReduce Framework: An Approach with Right Inverse Proceedings of International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR) Proceedings of International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR) Proceedings of International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR) 2014/09 Refereed English Research paper(international conference proceedings) Disclose to all
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 Refereed Disclose to all
Kohei Suenaga, Hiroyoshi Sekine, Ichiro Hasuo Kohei Suenaga, Hiroyoshi Sekine, Ichiro Hasuo Kohei Suenaga, Hiroyoshi Sekine, Ichiro 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 ACM SIGPLAN Notices, 48, 1, 417-430 ACM SIGPLAN Notices, 48, 1, 417-430 ACM SIGPLAN Notices, 48, 1, 417-430 2013/01 Refereed English Research paper(international conference proceedings) Disclose to all
Kohei Suenaga, Hiroyoshi Sekine, Ichiro Hasuo Kohei Suenaga, Hiroyoshi Sekine, Ichiro Hasuo Kohei Suenaga, Hiroyoshi Sekine, Ichiro 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 Refereed English Research paper(international conference proceedings) Disclose to all
Kohei Suenaga, Ryota Fukuda, Atsushi Igarashi Kohei Suenaga, Ryota Fukuda, Atsushi Igarashi Kohei Suenaga, Ryota Fukuda, Atsushi 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 ACM SIGPLAN Notices, 47, 10, 1-20 ACM SIGPLAN Notices, 47, 10, 1-20 ACM SIGPLAN Notices, 47, 10, 1-20 2012/10 Refereed English Research paper(international conference proceedings) Disclose to all
Kohei Suenaga, Ryota Fukuda, Atsushi Igarashi Kohei Suenaga, Ryota Fukuda, Atsushi Igarashi Kohei Suenaga, Ryota Fukuda, Atsushi 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 ACM SIGPLAN NOTICES, 47, 10, 1-20 ACM SIGPLAN NOTICES, 47, 10, 1-20 ACM SIGPLAN NOTICES, 47, 10, 1-20 2012/10 Refereed English Research paper(scientific journal) Disclose to all
Ichiro Hasuo, Kohei Suenaga Ichiro Hasuo, Kohei Suenaga Ichiro Hasuo, Kohei 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 Refereed English Research paper(international conference proceedings) Disclose to all
Ryosuke Sato, Kohei Suenaga, Naoki Kobayashi Ryosuke Sato, Kohei Suenaga, Naoki Kobayashi Ryosuke Sato, Kohei Suenaga, Naoki Kobayashi 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 Refereed English Research paper(scientific journal) Disclose to all
Kohei Suenaga, Ichiro Hasuo Kohei Suenaga, Ichiro Hasuo Kohei Suenaga, Ichiro 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 Automata, Languages and Programming, ICALP, Pt II, 6756, 392-403 Automata, Languages and Programming, ICALP, Pt II, 6756, 392-403 Automata, Languages and Programming, ICALP, Pt II, 6756, 392-403 2011 Refereed English Research paper(international conference proceedings) Disclose to all
Sato Ryosuke, Suenaga Kohei, Kobayashi Naoki 佐藤 亮介, 末永 幸平, 小林 直樹 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 English Disclose to all
Kohei Suenaga, Naoki Kobayashi Kohei Suenaga, Naoki Kobayashi Kohei Suenaga, Naoki Kobayashi Fractional Ownerships for Safe Memory Deallocation Fractional Ownerships for Safe Memory Deallocation Fractional Ownerships for Safe Memory Deallocation PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS, 5904, 128-143 PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS, 5904, 128-143 PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS, 5904, 128-143 2009 Refereed English Research paper(international conference proceedings) Disclose to all
飯村 枝里, 小林 直樹, 末永 幸平 飯村 枝里, 小林 直樹, 末永 幸平 飯村 枝里, 小林 直樹, 末永 幸平 Identifying Deadlock Errors by Type Error Slicing 型エラースライシングによるデッドロックの原因特定 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 Japanese Disclose to all
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, PROCEEDINGS, 5356, 155-170 PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS, 5356, 155-170 PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS, 5356, 155-170 2008 Refereed English Research paper(international conference proceedings) Disclose to all
Koichi Kodama, Kohei Suenaga, Naoki Kobayashi Koichi Kodama, Kohei Suenaga, Naoki Kobayashi Koichi Kodama, Kohei Suenaga, Naoki 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 J. Funct. Program., 18, 3, 333-371 J. Funct. Program., 18, 3, 333-371 J. Funct. Program., 18, 3, 333-371 2008 Refereed English Research paper(scientific journal) Disclose to all
Kohei Suenaga, Naoki Kobayashi Kohei Suenaga, Naoki Kobayashi Kohei Suenaga, Naoki Kobayashi 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, PROCEEDINGS, 4421, 490-+ PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS, 4421, 490-+ PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS, 4421, 490-+ 2007 Refereed English Research paper(international conference proceedings) Disclose to all
Kohei Suenaga, Naoki Kobayashi, Akinori Yonezawa Kohei Suenaga, Naoki Kobayashi, Akinori Yonezawa Kohei Suenaga, Naoki Kobayashi, 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, 3901, 98-114 LOGIC BASED PROGRAM SYNTHESIS AND TRANSFORMATION, 3901, 98-114 LOGIC BASED PROGRAM SYNTHESIS AND TRANSFORMATION, 3901, 98-114 2006 Refereed English Research paper(scientific journal) Disclose to all
Naoki Kobayashi, Kohei Suenaga, Lucian Wischik Naoki Kobayashi, Kohei Suenaga, Lucian Wischik Naoki Kobayashi, 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, 3 CoRR, abs/cs/0608035, 3 CoRR, abs/cs/0608035, 3 2006 Refereed English Research paper(scientific journal) Disclose to all
N Kobayashi, K Suenaga, L Wischik N Kobayashi, K Suenaga, L Wischik N Kobayashi, K Suenaga, L 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, PROCEEDINGS, 3855, 298-312 VERIFICATION, MODEL CHECKING , AND ABSTRACT INTERPRETATION, PROCEEDINGS, 3855, 298-312 VERIFICATION, MODEL CHECKING , AND ABSTRACT INTERPRETATION, PROCEEDINGS, 3855, 298-312 2006 Refereed English Research paper(scientific journal) Disclose to all
Naoki Kobayashi, Kohei Suenaga, Lucian Wischik Naoki Kobayashi, Kohei Suenaga, Lucian Wischik Naoki Kobayashi, 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 Refereed English Research paper(scientific journal) Disclose to all
K Suenaga, Y Oiwa, E Sumii, A Yonezawa K Suenaga, Y Oiwa, E Sumii, A Yonezawa K Suenaga, Y Oiwa, E Sumii, A 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, 3233, 192-208 SOFTWARE SECURITY - THEORIES AND SYSTEMS, 3233, 192-208 SOFTWARE SECURITY - THEORIES AND SYSTEMS, 3233, 192-208 2004 Refereed English Research paper(scientific journal) Disclose to all
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 PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS, 3302, 41-56 PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS, 3302, 41-56 PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS, 3302, 41-56 2004 Refereed English Research paper(scientific journal) Disclose to all
末永幸平, 大岩寛, 住井英二郎, 米澤明憲 末永幸平, 大岩寛, 住井英二郎, 米澤明憲 末永幸平, 大岩寛, 住井英二郎, 米澤明憲 Fail-Safe Cのためのインターフェイス定義言語 Fail-Safe Cのためのインターフェイス定義言語 Fail-Safe Cのためのインターフェイス定義言語 第5回プログラミングおよびプログラミング言語ワークショップ(PPL 2003)論文集, 135-148 第5回プログラミングおよびプログラミング言語ワークショップ(PPL 2003)論文集, 135-148 第5回プログラミングおよびプログラミング言語ワークショップ(PPL 2003)論文集, 135-148 2003 Refereed Japanese Research paper(other academic) Disclose to all
蓮尾 一郎, 末永 幸平 蓮尾 一郎, 末永 幸平 CPSの形式検証——超準解析によるアプローチ CPSの形式検証——超準解析によるアプローチ 計測と制御, 53, 12, 1-6 計測と制御, 53, 12, 1-6 , 53, 12, 1-6 Refereed Japanese Research paper(scientific journal) Disclose to all

  • <<
  • >>
Title language:
Misc
Author Author(Japanese) Author(English) Title Title(Japanese) Title(English) Bibliography Bibliography(Japanese) Bibliography(English) Publication date Refereed paper Language Publishing type Disclose
Ichiro Hasuo, Yuichiro Oyabu, Clovis Eberhart, Kohei Suenaga, Kenta Cho, Shin-ya Katsumata Ichiro Hasuo, Yuichiro Oyabu, Clovis Eberhart, Kohei Suenaga, Kenta Cho, Shin-ya Katsumata Ichiro Hasuo, Yuichiro Oyabu, Clovis Eberhart, Kohei Suenaga, Kenta Cho, Shin-ya Katsumata Hierarchical Sampler for Probabilistic Programs via Separation of Control and Data Hierarchical Sampler for Probabilistic Programs via Separation of Control and Data Hierarchical Sampler for Probabilistic Programs via Separation of Control and Data 2021/01/05 Disclose to all
Yuhki Hatakeyama, Hiroki Sakuma, Yoshinori Konishi, Kohei Suenaga Yuhki Hatakeyama, Hiroki Sakuma, Yoshinori Konishi, Kohei Suenaga Yuhki Hatakeyama, Hiroki Sakuma, Yoshinori Konishi, Kohei Suenaga Visualizing Color-wise Saliency of Black-Box Image Classification Models. Visualizing Color-wise Saliency of Black-Box Image Classification Models. Visualizing Color-wise Saliency of Black-Box Image Classification Models. CoRR, abs/2010.02468 CoRR, abs/2010.02468 CoRR, abs/2010.02468 2020 Disclose to all
今西 諒文, 関山 太朗, 村主 崇行, 末永 幸平 今西 諒文, 関山 太朗, 村主 崇行, 末永 幸平 深層学習によるプログラム生成の高速化 深層学習によるプログラム生成の高速化 第19回プログラミングおよびプログラミング言語ワークショップ, 第19回プログラミングおよびプログラミング言語ワークショップ, 2017 Japanese Other Disclose to all
五十嵐 淳, 中澤 巧爾, 馬谷 誠二, 関山 太朗, 花田 裕一朗, 大元 武, 宮本 洋平, 末永 幸平 五十嵐 淳, 中澤 巧爾, 馬谷 誠二, 関山 太朗, 花田 裕一朗, 大元 武, 宮本 洋平, 末永 幸平 京都大学 Teen Racketeer 養成コース 京都大学 Teen Racketeer 養成コース 第17回プログラミングおよびプログラミング言語ワークショップ 第17回プログラミングおよびプログラミング言語ワークショップ 2015 Japanese Other Disclose to all
Title language:
Conference Activities & Talks
Title Title(Japanese) Title(English) Conference Conference(Japanese) Conference(English) Promotor Promotor(Japanese) Promotor(English) Date Language Assortment Disclose
物理情報システムに対するブラックボックス検査の構文的仕様強化による最適化 物理情報システムに対するブラックボックス検査の構文的仕様強化による最適化 第23回プログラミングおよびプログラミング言語ワークショップ (PPL 2021) 第23回プログラミングおよびプログラミング言語ワークショップ (PPL 2021) 2021/03/10 Japanese Poster presentation Disclose to all
暗号通貨向けストレージシステムにおけるデータ永続化処理の形式検証 暗号通貨向けストレージシステムにおけるデータ永続化処理の形式検証 第23回プログラミングおよびプログラミング言語ワークショップ (PPL 2021) 第23回プログラミングおよびプログラミング言語ワークショップ (PPL 2021) 2021/03/09 Japanese Poster presentation Disclose to all
Visualizing Color-Wise Saliency of Black-Box Image Classification Models Visualizing Color-Wise Saliency of Black-Box Image Classification Models Visualizing Color-Wise Saliency of Black-Box Image Classification Models ACCV 2020 ACCV 2020 ACCV 2020 Disclose to all
ブラックボックス画像分類モデルの否定的判断根拠と色情報根拠の可視化 ブラックボックス画像分類モデルの否定的判断根拠と色情報根拠の可視化 MIRU 2020 MIRU 2020 Japanese Poster presentation Disclose to all
F*を用いたMerkle Patricia Treeライブラリの形式検証 F*を用いたMerkle Patricia Treeライブラリの形式検証 PPL 2020 PPL 2020 Japanese Oral presentation(general) Disclose to all
スマートコントラクトのための Effectively Callback-Free 性の型に基づく静的検証 スマートコントラクトのための Effectively Callback-Free 性の型に基づく静的検証 PPL 2020 PPL 2020 Japanese Oral presentation(general) Disclose to all
Generalized Property-Directed Reachability for Hybrid Systems Generalized Property-Directed Reachability for Hybrid Systems Generalized Property-Directed Reachability for Hybrid Systems VMCAI 2020 VMCAI 2020 VMCAI 2020 2020/01/19 English Oral presentation(general) Disclose to all
軽量なプログラム検証のための要素技術[Invited] 軽量なプログラム検証のための要素技術 [Invited] 国立情報学研究所 オープンハウス2019:産官学連携セミナー 「形式手法・ソフトウェア工学の先端とさらに先:効率的テスト手法と機械学習・人工知能協働」 国立情報学研究所 オープンハウス2019:産官学連携セミナー 「形式手法・ソフトウェア工学の先端とさらに先:効率的テスト手法と機械学習・人工知能協働」 2019/05/31 Japanese Public discourse, seminar, tutorial, course, lecture and others Disclose to all
安全性検証技術はビジネスになるか[Invited] 安全性検証技術はビジネスになるか [Invited] 第6回 Entrepreneur Candidate Club(ECC-iCAP) the place where science & entrepreneurship intersect ~科学のフロントランナーが語る未来世界~ 第6回 Entrepreneur Candidate Club(ECC-iCAP) the place where science & entrepreneurship intersect ~科学のフロントランナーが語る未来世界~ 2019/05/17 Japanese Public discourse, seminar, tutorial, course, lecture and others Disclose to all
Automated proof synthesis for propositional logic using deep learning[Invited] Automated proof synthesis for propositional logic using deep learning [Invited] Automated proof synthesis for propositional logic using deep learning [Invited] 5th France-Japan Cybersecurity workshop 5th France-Japan Cybersecurity workshop 5th France-Japan Cybersecurity workshop 2019/04/23 English Oral presentation(general) Disclose to all
日本語契約書の一般的な構造定義に向けて 日本語契約書の一般的な構造定義に向けて 2019/03/13 Japanese Oral presentation(general) Disclose to all
Automated Proof Synthesis for the Minimal Propositional Logic with Deep Neural Networks Automated Proof Synthesis for the Minimal Propositional Logic with Deep Neural Networks Automated Proof Synthesis for the Minimal Propositional Logic with Deep Neural Networks APLAS 2018 APLAS 2018 APLAS 2018 2018/12/03 English Oral presentation(general) Disclose to all
Property-Directed Reachability for Hybrid Systems with Differential Dynamic Logic Predicates Property-Directed Reachability for Hybrid Systems with Differential Dynamic Logic Predicates Property-Directed Reachability for Hybrid Systems with Differential Dynamic Logic Predicates APLAS 2018 Student Research Competition APLAS 2018 Student Research Competition APLAS 2018 Student Research Competition 2018/12/02 English Poster presentation Disclose to all
ニューラルネットワークによるフォトニック結晶格子点構造の3次元モデリングの検討 ニューラルネットワークによるフォトニック結晶格子点構造の3次元モデリングの検討 第65回応用物理学会春季学術講演会 第65回応用物理学会春季学術講演会 2018/03/20 Japanese Poster presentation Disclose to all
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 English Oral presentation(general) Disclose to all
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 English Poster presentation Disclose to all
超準プログラミング言語を用いたハイブリッドシステムのモデリングと検証[Invited] 超準プログラミング言語を用いたハイブリッドシステムのモデリングと検証 [Invited] 第9回 暗号及び情報セキュリティと数学の相関ワークショップ (CRISMATH 2017) 第9回 暗号及び情報セキュリティと数学の相関ワークショップ (CRISMATH 2017) 2017/12/22 Japanese Oral presentation(invited, special) Disclose to all
A Nonstandard Functional Programming Language A Nonstandard Functional Programming Language A Nonstandard Functional Programming Language APLAS 2017 APLAS 2017 APLAS 2017 2017/11/27 English Oral presentation(general) Disclose to all
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 English Oral presentation(general) Disclose to all
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 English Oral presentation(general) Disclose to all
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 English Oral presentation(general) Disclose to all
超準関数型プログラミング言語NSF 超準関数型プログラミング言語NSF 第19回プログラミングおよびプログラミング言語ワークショップ(PPL2017) 第19回プログラミングおよびプログラミング言語ワークショップ(PPL2017) 2017/03/08 Japanese Poster presentation Disclose to all
深層学習によるプログラム生成の高速化 深層学習によるプログラム生成の高速化 第19回プログラミングおよびプログラミング言語ワークショップ(PPL2017) 第19回プログラミングおよびプログラミング言語ワークショップ(PPL2017) 2017/03/08 Japanese Poster presentation Disclose to all
無限状態システムのHFLモデル検査のための型に基づく手法 無限状態システムのHFLモデル検査のための型に基づく手法 第19回プログラミングおよびプログラミング言語ワークショップ(PPL2017) 第19回プログラミングおよびプログラミング言語ワークショップ(PPL2017) 2017/03/08 Japanese Poster presentation Disclose to all
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 Oral presentation(general) Disclose to all
そのプログラム、バグってないですか?:数学を使ってバグを見つけるための形式検証手法[Invited] そのプログラム、バグってないですか?:数学を使ってバグを見つけるための形式検証手法 [Invited] 2016年度情報処理学会関西支部定期講演会「IoT の周辺技術」 2016年度情報処理学会関西支部定期講演会「IoT の周辺技術」 2016/12/21 Public discourse, seminar, tutorial, course, lecture and others Disclose to all
超準解析を用いたハイブリッドシステム検証手法[Invited] 超準解析を用いたハイブリッドシステム検証手法 [Invited] 統計数理解析研究所シンポジウム --- 工学と現代数学の接点を求めて 統計数理解析研究所シンポジウム --- 工学と現代数学の接点を求めて 2016/12/20 Symposium workshop panel(nominated) Disclose to all
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 English Oral presentation(general) Disclose to all
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 English Oral presentation(general) Disclose to all
ソフトウェアのための自動形式検証ツール ソフトウェアのための自動形式検証ツール ET/IoT 総合技術展 関西(ETWest 2016) ET/IoT 総合技術展 関西(ETWest 2016) 2016/07/07 Japanese Poster presentation Disclose to all
そのプログラム、バグってないですか? ― 数学を使ってバグを見つける[Invited] そのプログラム、バグってないですか? ― 数学を使ってバグを見つける [Invited] JST 京都大学新技術説明会 JST 京都大学新技術説明会 2016/05/24 Japanese Public discourse, seminar, tutorial, course, lecture and others Disclose to all
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 English Public discourse, seminar, tutorial, course, lecture and others Disclose to all
Nonstandard Analysis Meets Programming Language Theory[Invited] Nonstandard Analysis Meets Programming Language Theory [Invited] Nonstandard Analysis Meets Programming Language Theory [Invited] 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 English Oral presentation(invited, special) Disclose to all
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 English Oral presentation(general) Disclose to all
Type-Based Safe Resource Deallocation for Shared-Memory Concurrency[Invited] Type-Based Safe Resource Deallocation for Shared-Memory Concurrency [Invited] 日本ソフトウェア科学会第30回大会特別招待講演 日本ソフトウェア科学会第30回大会特別招待講演 2013/09/12 Japanese Oral presentation(invited, special) Disclose to all
形式検証手法は無限小プログラミングを使えばハイブリッドシステムにもそのまま使える[Invited] 形式検証手法は無限小プログラミングを使えばハイブリッドシステムにもそのまま使える [Invited] 日本ソフトウェア科学会第30回大会Future Technology Design (FTD) 2013 日本ソフトウェア科学会第30回大会Future Technology Design (FTD) 2013 2013/09/11 Japanese Oral presentation(invited, special) Disclose to all
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 English Oral presentation(general) Disclose to all

  • <<
  • >>
Title language:
Industrial Property Rights (Patent)
Inventor(s) Inventor(s) (Japanese) Inventor(s) (English) Title Title(Japanese) Title(English) Stage Patent number Date Disclose
蓮尾 一郎, 奥殿 貴仁, 木戸 肩吾, 末永 幸平, 小島 健介, 西田 雄気 蓮尾 一郎, 奥殿 貴仁, 木戸 肩吾, 末永 幸平, 小島 健介, 西田 雄気 自動証明装置、及びプログラム 自動証明装置、及びプログラム 特許公開 特開2019-020966 2019/02/07 Disclose to all
末永 幸平, 今西 諒文, 五十嵐 淳 末永 幸平, 今西 諒文, 五十嵐 淳 プログラム検証装置、プログラム検証方法、プログラム検証のためのコンピュータプログラム、 プログラム変換器、プログラム変換方 法、プログラム変換のためのコンピュータプログラム、 プログラム製造方法、及び検証用プログラム プログラム検証装置、プログラム検証方法、プログラム検証のためのコンピュータプログラム、 プログラム変換器、プログラム変換方 法、プログラム変換のためのコンピュータプログラム、 プログラム製造方法、及び検証用プログラム 特許出願 PCT/JP2018/044029 2018/11/29 Disclose to all
末永 幸平, 今西 諒文, 五十嵐 淳 末永 幸平, 今西 諒文, 五十嵐 淳 プログラム検証装置、プログラム検証方法、プログラム検証のためのコンピュータプログラム、プログラム変換器、プログラム変換方法、プログラム変換のためのコンピュータプログラム、プログラム製造方法、及び検証用プログラム プログラム検証装置、プログラム検証方法、プログラム検証のためのコンピュータプログラム、プログラム変換器、プログラム変換方法、プログラム変換のためのコンピュータプログラム、プログラム製造方法、及び検証用プログラム 特許出願 特願2017-246154 2017/12/22 Disclose to all
末永 幸平, 樹下 稔, 小島 健介 末永 幸平, 樹下 稔, 小島 健介 不変条件生成装置、コンピュータプログラム、不変条件生成方法、プログラムコード製造方法 不変条件生成装置、コンピュータプログラム、不変条件生成方法、プログラムコード製造方法 特許登録 特許6632058 Disclose to all
末永 幸平, 樹下 稔, 小島 健介 末永 幸平, 樹下 稔, 小島 健介 不変条件生成装置、コンピュータプログラム、不変条件生成方法、プログラムコード製造方法 不変条件生成装置、コンピュータプログラム、不変条件生成方法、プログラムコード製造方法 特許登録 特許6622098 Disclose to all
樹下稔, 小島健介, 末永幸平 樹下稔, 小島健介, 末永幸平 不変条件生成装置、コンピュータプログラム、不変条件生成方法、プログラムコード製造方法 不変条件生成装置、コンピュータプログラム、不変条件生成方法、プログラムコード製造方法 特許出願 PCT/JP2017/003295 2017/01/31 Disclose to all
末永 幸平, 蓮尾 一郎 末永 幸平, 蓮尾 一郎 ハイブリッドシステムの検証方法、検証装置、及び検証コンピュータプログラム、並びに、ハイブリッドシステムのモデル変換方法、変換装置、及び変換コンピュータプログラム ハイブリッドシステムの検証方法、検証装置、及び検証コンピュータプログラム、並びに、ハイブリッドシステムのモデル変換方法、変換装置、及び変換コンピュータプログラム 特許登録 特許第5843230号 2015/11/27 Disclose to all
蓮尾 一郎, 赤崎 拓未, 末永 幸平 蓮尾 一郎, 赤崎 拓未, 末永 幸平 制御入力値生成装置、制御入力値生成方法、および、プログラム 制御入力値生成装置、制御入力値生成方法、および、プログラム 特許公開 特開2015-194917 2015/11/05 Disclose to all
赤崎 拓未, 蓮尾 一郎, 末永 幸平 赤崎 拓未, 蓮尾 一郎, 末永 幸平 制御入力値生成装置,制御入力値生成方法,および,プログラム 制御入力値生成装置,制御入力値生成方法,および,プログラム 特許出願 特願2014-72623 2014/03/31 Disclose to all
Hiroaki Nakamura, Hisashi Miyashita, Kohei Suenaga 中村 宏明, 宮下 尚, 末永 幸平 Hiroaki Nakamura, Hisashi Miyashita, Kohei Suenaga INFORMATION MANAGEMENT SYSTEM, METHOD AND PROGRAM 情報管理システム、方法及びプログラム INFORMATION MANAGEMENT SYSTEM, METHOD AND PROGRAM 特許登録 特許第5431261号 2013/12/13 Disclose to all
Title language:
Awards
Title(Japanese) Title(English) Organization name(Japanese) Organization name(English) Date
PPL 2007 発表賞 日本ソフトウェア科学会プログラミング論研究会 2007/03/
PPL 2009 発表賞 日本ソフトウェア科学会プログラミング論研究会 2009/03/
PPL 2012 発表賞 日本ソフトウェア科学会プログラミング論研究会 2012/03/
Journal of Information Processing Outstanding Paper Award 情報処理学会 2012/06/
External funds: competitive funds and Grants-in-Aid for Scientific Research (Kakenhi)
Type Position Title(Japanese) Title(English) Period
特別研究員奨励費 並行プログラムのための型理論に基づく利便性の高い静的検証手法 2011-2011
研究活動スタート支援 Representative 無限小プログラミングによるハイブリッドシステムの形式検証手法 2012-2013
若手研究(B) Representative 無限小プログラミングによるハイブリッドシステムの形式検証手法 2013-2015
若手研究(B) Representative 無限小プログラミングによるハイブリッドシステムの形式検証手法 (平成26年度分) 2014/04/01-2015/03/31
若手研究(B) Representative 無限小プログラミングによるハイブリッドシステムの形式検証手法 (平成27年度分) 2015/04/01-2016/03/31
挑戦的研究(萌芽) Representative 数学の自動化を推進するための機械学習を用いた定理自動証明手法 2019/08/01-2022/03/31
基盤研究(B) Representative IoT システムのための形式検証手法の深化 2019/04/01-2024/03/31
基盤研究 (B) Assignment 圏論と数理論理学によるものづくりサポート―ソフトウェア科学のシステム工学への移転 2015/04/01-2020/03/31
挑戦的研究(萌芽) Representative 数学の自動化を推進するための機械学習を用いた定理自動証明手法 (2019年度分) 2019/04/01-2020/03/31
基盤研究(B) Representative IoT システムのための形式検証手法の深化 (2019年度分) 2019/04/01-2020/03/31
挑戦的研究(萌芽) Representative 数学の自動化を推進するための機械学習を用いた定理自動証明手法 (2020年度分) 2020/04/01-2021/03/31
基盤研究(B) Representative IoT システムのための形式検証手法の深化 (2020年度分) 2020/04/01-2021/03/31
基盤研究(B) Representative IoT システムのための形式検証手法の深化 (2020年度分) 2020/04/01-2021/03/31

  • <<
  • >>
External funds: other than those above
System Main person Title(Japanese) Title(English) Period
JST さきがけ 末永幸平 ハイブリッドシステムのための超準プログラミング言語理論を用いた形式手法 Formal methods for hybrid systems based on the theory of nonstandard programming langauges 2015/10/01-2019/03/31
JST CREST 末永幸平 AI集約的サイバーフィジカルシステムの形式的解析手法 CyPhAI: Formal Analysis and Design of AI-intenstive Cyber-PHysical SYstems 2020/11/01-2025/03/31
Teaching subject(s)
Name(Japanese) Name(English) Term Department Period
計算機科学実験及演習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
並列分散システム論 Parallel and Distributed Systems 前期 情報学研究科 2019/04-2020/03
プログラム意味論 Formal Semantics of Computer Programs 前期 情報学研究科 2019/04-2020/03
プログラミング言語処理系 Implementation of Programming Languages 前期 工学部 2019/04-2020/03
計算機科学実験及演習3 Computer Science Laboratory and Exercise 3 前期 工学部 2019/04-2020/03
計算機科学のための数学演習 Mathematics in Practice for Computer Science 前期 工学部 2019/04-2020/03
並列分散システム論 Parallel and Distributed Systems 後期 情報学研究科 2020/04-2021/03
プログラム意味論 Formal Semantics of Computer Programs 前期 情報学研究科 2020/04-2021/03
プログラミング言語処理系 Implementation of Programming Languages 前期 工学部 2020/04-2021/03
計算機科学実験及演習3(計算機) Computer Science Laboratory and Exercise 3 前期 工学部 2020/04-2021/03
計算機科学のための数学演習 Mathematics in Practice for Computer Science 前期 工学部 2020/04-2021/03
プログラム意味論 Formal Semantics of Computer Programs 前期 情報学研究科 2021/04-2022/03
システム検証論 System Verification 後期 情報学研究科 2021/04-2022/03
プログラミング言語処理系 Implementation of Programming Languages 前期 工学部 2021/04-2022/03
計算機科学実験及演習3(計算機) Computer Science Laboratory and Exercise 3 前期 工学部 2021/04-2022/03

  • <<
  • >>
Faculty management (title, position)
Title Period
情報セキュリティ作業委員会委員 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
図書WG 2020/04/01-2022/03/31
連携推進WG委員 2021/04/01-2022/03/31

  • <<
  • >>
Other activities (awards)
Award name Organization name Date
京都大学学際研究着想コンテスト優秀賞 京都大学 2013/09/
Other activities (private companies, NPOs, etc.)
Company name Activity Period
Patentfield株式会社 技術顧問 2017/06/01-
株式会社LegalForce 学術指導 2018/02/01-
ダイラムダ株式会社 技術顧問 2019/05/01-
株式会社センスタイムジャパン 技術顧問 2019/05/01-