Rchr
J-GLOBAL ID:201401093199514640   Update date: Aug. 06, 2021

Suenaga Kohei

スエナガ コウヘイ | Suenaga Kohei
Affiliation and department:
Job title: Associate Professor
Other affiliations (1):
Homepage URL  (1): http://www.fos.kuis.kyoto-u.ac.jp/~ksuenaga/
Research field  (1): Software
Research keywords  (8): 静的検証 ,  超準解析 ,  形式手法 ,  型システム ,  ホーア論理 ,  プログラミング言語 ,  無限小プログラミング ,  ハイブリッドシステム
Research theme for competitive and other funds  (14):
  • 2020 - 2025 Research on software contracts for highly interoperable software modules
  • 2020 - 2025 CyPhAI: Formal Analysis and Design of AI-intensive Cyber-Physical Systems
  • 2019 - 2024 IoT システムのための形式検証手法の深化
  • 2019 - 2022 数学の自動化を推進するための機械学習を用いた定理自動証明手法
  • 2019 - 2022 数学の自動化を推進するための機械学習を用いた定理自動証明手法
Show all
Papers (54):
  • Takeshi Tsukada, Hiroshi Unno 0001, Taro Sekiyama, Kohei Suenaga. Enhancing Loop-Invariant Synthesis via Reinforcement Learning. CoRR. 2021. abs/2107.09766
  • Sota Sato, Ryotaro Banno, Jun Furuse, Kohei Suenaga, Atsushi Igarashi. Verification of a Merkle Patricia Tree Library Using F. CoRR. 2021. abs/2106.04826
  • 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. CoRR. 2021. abs/2101.01502
  • 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. Proceedings of TACAS 2021. 2021. 262-280
  • 齋藤 大聖, 西田 雄気, 五十嵐 淳, 末永 幸平. スマートコントラクトのための Effectively Callback-Free 性の型に基づく静的検証. PPL 2020. 2020
more...
MISC (4):
  • Ichiro Hasuo, Yuichiro Oyabu, Clovis Eberhart, Kohei Suenaga, Kenta Cho, Shin-ya Katsumata. Hierarchical Sampler for Probabilistic Programs via Separation of Control and Data. 2021
  • Yuhki Hatakeyama, Hiroki Sakuma, Yoshinori Konishi, Kohei Suenaga. Visualizing Color-wise Saliency of Black-Box Image Classification Models. CoRR. 2020. abs/2010.02468
  • 今西 諒文, 関山 太朗, 村主 崇行, 末永 幸平. 深層学習によるプログラム生成の高速化. 第19回プログラミングおよびプログラミング言語ワークショップ,. 2017
  • 五十嵐 淳, 中澤 巧爾, 馬谷 誠二, 関山 太朗, 花田 裕一朗, 大元 武, 宮本 洋平, 末永 幸平. 京都大学 Teen Racketeer 養成コース. 第17回プログラミングおよびプログラミング言語ワークショップ. 2015
Patents (10):
more...
Lectures and oral presentations  (37):
  • 物理情報システムに対するブラックボックス検査の構文的仕様強化による最適化
    (第23回プログラミングおよびプログラミング言語ワークショップ (PPL 2021) 2021)
  • 暗号通貨向けストレージシステムにおけるデータ永続化処理の形式検証
    (第23回プログラミングおよびプログラミング言語ワークショップ (PPL 2021) 2021)
  • Visualizing Color-Wise Saliency of Black-Box Image Classification Models
    (ACCV 2020)
  • ブラックボックス画像分類モデルの否定的判断根拠と色情報根拠の可視化
    (MIRU 2020)
  • F*を用いたMerkle Patricia Treeライブラリの形式検証
    (PPL 2020)
more...
Education (5):
  • 2005 - 2008 The University of Tokyo Department of Computer Science
  • 2003 - 2005 The University of Tokyo Department of Computer Science
  • 2000 - 2003 The University of Tokyo Department of Information Science
  • 1998 - 2000 The University of Tokyo
  • 1995 - 1998 宮崎県立宮崎西高等学校 理数科
Professional career (1):
  • 博士(情報理工学) (東京大学)
Work history (14):
  • 2019/09 - 現在 Social System Design Center Advisor
  • 2019/05 - 現在 SenseTime Japan Ltd. Advisor
  • 2019/05 - 現在 DaiLambda, Inc. Advisor
  • 2017/06 - 現在 Patentfield Inc. Scientific Advisor
  • 2017/04 - 現在 LegalForce Inc. Advisor
Show all
Committee career (21):
  • 2019/04 - 現在 日本ソフトウェア科学会プログラミング論研究会 運営委員
  • 2017/04 - 現在 情報処理学会関西支部 支部委員
  • 2013/07 - 現在 文部科学省科学技術政策研究所科学技術動向研究センター 専門調査員
  • 2012/02 - 現在 情報処理学会 若手研究者の会
  • 2019/10 - 2020/04 5th Workshop on Monitoring and Testing of Cyber-Physical Systems (MT-CPS 2020) プログラム共同委員長
Show all
Awards (5):
  • 2013/09 - 京都大学 京都大学学際研究着想コンテスト優秀賞 視覚・聴覚に続く第三の電子媒体「匂い」--その時代に備えるための技術革新と社会環境整備
  • 2012/06 - IPSJ Journal of Information Processing Outstanding Paper Award Ordered types for stream processing of tree-structured data. Journal of Information Processing
  • 2012/03 - 日本ソフトウェア科学会プログラミング論研究会 PPL 2012 発表賞 Programming with infinitesimals: A WHILE-language for hybrid system modeling
  • 2009/03 - 日本ソフトウェア科学会プログラミング論研究会 PPL 2009 発表賞 Type-based deadlock-freedom verification for non-block-structured lock primitives and mutable references
  • 2007/03 - 日本ソフトウェア科学会プログラミング論研究会 PPL 2007 発表賞 Type-based analysis of deadlock for a concurrent calculus with interrupts
Association Membership(s) (3):
IPSJ ,  JSSST ,  ACM
※ Researcher’s information displayed in J-GLOBAL is based on the information registered in researchmap. For details, see here.

Return to Previous Page