Basic Information

Faculty

• 工学部 工学部

Professional Memberships

• IPSJ
• JSSST
• ACM

Academic Degree

• 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)

• The University of Tokyo, 大学院情報理工学系研究科コンピュータ科学専攻修士課程, 修了
• The University of Tokyo, 大学院情報理工学系研究科コンピュータ科学専攻博士課程, 修了

Academic Resume (Undergraduate School/Majors)

• The University of Tokyo, 理学部情報科学科, 卒業
• The University of Tokyo, 教養学部理科一類

High School

• High School

  宮崎県立宮崎西高等学校

Research History

• From Sep. 2019, To Present

  Social System Design Center, Advisor
• From May 2019, To Present

  SenseTime Japan Ltd., Advisor
• From May 2019, To Present

  DaiLambda, Inc., Advisor
• From Jun. 2017, To Present

  Patentfield Inc., Scientific Advisor
• From Apr. 2017, To Present

  LegalForce Inc., Advisor
• From Oct. 2013, To Present

  Kyoto University, Graduate School of Informatics, Associate Professor
• From Oct. 2015, To Mar. 2019

  JST PRESTO, Researcher
• From Apr. 2012, To Sep. 2013

  Kyoto University, The Hakubi Center for Advanced Research, Assistant Professor
• From Apr. 2011, To Mar. 2012

  日本学術振興会, 特別研究員 (PD)
• From Feb. 2011, To Mar. 2011

  Kyoto University, Graduate School of Informatics, Program-specific Researcher
• From Apr. 2010, To Jan. 2011

  Universidade de Lisboa, Faculdade de Ciencia, Investigador pos-doutorado
• From Apr. 2009, To Mar. 2010

  IBM, IBM Research, Tokyo, Researcher
• From Apr. 2008, To Mar. 2009

  日本学術振興会, 特別研究員 (PD)
• From Apr. 2007, To Mar. 2008

  日本学術振興会, 特別研究員 (DC2)

Profile

• Profile

  He completed the doctoral program in Computer Science at the Graduate School of Information Science and Technology, the University of Tokyo, in 2008. Ph.D. (Information Science and Technology). After serving as a JSPS Research Fellow (DC2, PD), a researcher at IBM Research--Tokyo (IBM Japan, Ltd.), a postdoctoral researcher at the Faculty of Sciences, University of Lisbon, a JSPS Research Fellow (PD), and a Program-Specific Assistant Professor at the Hakubi Center, Kyoto University, became an Associate Professor at the Graduate School of Informatics, Kyoto University, in 2013, continuing to the present. He has also served as a Visiting Associate Professor at the National Institute of Informatics since 2018. Interested in formal verification methods for software systems, hybrid systems, machine learning systems, and smart contracts.

  
  

  I study formal verification of software. Using type theory, program logic, automata theory, and other approaches, I have worked on concurrent programs, hybrid systems, smart contracts, machine learning models, computation without decrypting data (such as homomorphic encryption), and programs that perform statistical hypothesis testing. My current goal is to develop techniques that guarantee correctness without relying on human effort, in an era where AI is building software. At Kyoto University, I teach courses such as "Implementation of Programming Languages" and make my teaching materials publicly available. I welcome cross-disciplinary collaboration.

Language of Instruction

• English
• Portuguese

ID,URL

• ORCID ID

  0000-0002-7466-8789

• J-Global ID

  201401093199514640

• Researcher number

  70633692

• External link

  https://ksuenaga.github.io/

researchmap URL

• https://researchmap.jp/ksuenaga

Research

Research Topics, Overview of the research

• Research Topics

  Formal verification

• Overview of the research

  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.

Research Interests

• 静的検証
• 超準解析
• 形式手法
• 型システム
• ホーア論理
• プログラミング言語
• 無限小プログラミング
• ハイブリッドシステム

Research Areas

• Informatics, Software

Papers

• Evaluating Hybrid Automata Learning Tools Based on Their Success in Formal Verification

  Niklas Kochdumper; Chiao Hsieh; Hadi Dayekh; Amit Gurung; Hidekazu Segawa; Thao Dang; Masaki Waga; Kohei Suenaga

  MED 2026 (Accepted), Jun. 2026, Peer-reviewed, Last author

  
• A Fast and Soft Pattern Matcher for Trillion-Scale Corpus

  Masataka Yoneda; Masataka_Yoneda; Yusuke Matsushita; Go Kamoda; Kohei Suenaga; Takuya Akiba; Masaki Waga; Sho Yokoi

  ICML 2026 (accepted), Jul. 2026, Peer-reviewed

  
• In-Situ Hardware Error Detection Using Specification-Derived Petri Net Models and Behavior-Derived State Sequences

  Tomonari Tanaka; Takumi Uezono; Kohei Suenaga; Masanori Hashimoto

  IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2026, Peer-reviewed

  
• Ownership Refinement Types for Pointer Arithmetic and Nested Arrays

  Yusuke Fujiwara; Yusuke Matsushita; Kohei Suenaga; Atsushi Igarashi

  ECOOP 2026, Jun. 2026, Peer-reviewed

  
• 制御フロー仕様から生成したペトリネットに基づくハードウェア誤動作検出手法

  田中 知成; 上薗 巧; 末永 幸平; 橋本 昌宜

  DAシンポジウム2024論文集, Aug. 2024

  
• Goal-Aware RSS for Complex Scenarios via Program Logic

  Ichiro Hasuo; Clovis Eberhart; James Haydon; Jérémy Dubut; Rose Bohrer; Tsutomu Kobayashi; Sasinee Pruekprasert; Xiao-Yi Zhang; Erik André Pallas; Akihisa Yamada; Kohei Suenaga; Fuyuki Ishikawa; Kenji Kamijo; Yoshiyuki Shinya; Takamasa Suetomi

  2024 IEEE Intelligent Vehicles Symposium (IV), 02 Jun. 2024

  
• SoftMatcha 2: 1 兆語規模コーパスの超高速かつ柔らかい検索

  米田優峻; 鴨田豪; 松下祐介; 末永幸平; 秋葉拓哉; 和賀正樹; 横井祥

  言語処理学会 第32回年次大会 発表論文集, Mar. 2026

  
• CHLOE: Loop Transformation over Fully Homomorphic Encryption via Multi-Level Vectorization and Control-Path Reduction.

  Song Bian; Zian Zhao; Ruiyu Shen; Zhou Zhang; Ran Mao; Dawei Li; Yizhong Liu; Masaki Waga; Kohei Suenaga; Zhenyu Guan; Jiafeng Hua; Yier Jin; Jianwei Liu

  IEEE Symposium on Security and Privacy(SP), 2025

  
• Active Learning of Symbolic Mealy Automata

  Kengo Irie; Masaki Waga; Kohei Suenaga

  ICTAC 2025, 2026, Peer-reviewed

  
• Efficient Black-Box Checking with Specification-Guided Abstraction

  Tsubasa Matsumoto; Kazuki Watanabe; Kohei Suenaga; Masaki Waga

  ACM Transactions on Embedded Computing Systems, 30 Sep. 2025, Peer-reviewed

  
• Componentwise Automata Learning for System Integration

  Hiroya Fujinami; Masaki Waga; Jie An; Kohei Suenaga; Nayuta Yanagisawa; Hiroki Iseri; Ichiro Hasuo

  ATVA 2025, 2026, Peer-reviewed

  
• HEIR: A Unified Representation for Cross-Scheme Compilation of Fully Homomorphic Computation.

  Song Bian; Zian Zhao; Zhou Zhang; Ran Mao; Kohei Suenaga; Yier Jin; Zhenyu Guan; Jianwei Liu

  31st Annual Network and Distributed System Security Symposium(NDSS), Sep. 2024, Peer-reviewed

  
• Sharper and Simpler Nonlinear Interpolants for Program Verification.

  Takamasa Okudono; Yuki Nishida 0001; Kensuke Kojima; Kohei Suenaga; Kengo Kido; Ichiro Hasuo

  Programming Languages and Systems - 15th Asian Symposium(APLAS), Dec. 2017, Peer-reviewed

  
• Certifying Lyapunov Stability of Black-Box Nonlinear Systems via Counterexample Guided Synthesis

  Chiao Hsieh; Masaki Waga; Kohei Suenaga

  HSCC 2025 (To appear), May 2025, Peer-reviewed

  
• A Soft and Fast Pattern Matcher for Billion-Scale Corpus Searches

  Hiroyuki Deguchi; Go Kamoda; Yusuke Matsushita; Chihiro Taguchi; Kohei Suenaga; Masaki Waga; Sho Yokoi

  ICLR 2025 (To appear), Apr. 2025, Peer-reviewed

  
• Oblivious Monitoring for Discrete-Time STL via Fully Homomorphic Encryption.

  Masaki Waga; Kotaro Matsuoka; Takashi Suwa; Naoki Matsumoto; Ryotaro Banno; Song Bian 0001; Kohei Suenaga

  Runtime Verification - 24th International Conference(RV), Oct. 2024, Peer-reviewed

  
• Hardware Error Detection with In-Situ Monitoring of Control Flow-Related Specifications

  Tomonari Tanaka; Takumi Uezono; Kohei Suenaga; Masanori Hashimoto

  Proceedings of the 30th Asia and South Pacific Design Automation Conference, 20 Jan. 2025

  Access this paper :

  
• iCon: Automated Verification of Inter-Transaction Properties in Tezos Smart Contracts with Unknowns

  Yuki Nishida; Kohei Suenaga; Atsushi Igarashi

  2024 IEEE International Conference on Blockchain and Cryptocurrency (ICBC), 27 May 2024, Peer-reviewed

  
• StatWhy: Formal Verification Tool for Statistical Hypothesis Testing Programs

  Yusuke Kawamoto; Kentaro Kobayashi; Kohei Suenaga

  CAV 2025, 22 Jul. 2025, Peer-reviewed

  
• 命令型プログラムの安全性検証のための所有権主導変換

  小林 亮太; 中村 烈士; 五十嵐 淳; 末永 幸平; 小林 直樹

  PPL 2024 論文集, Mar. 2024, Peer-reviewed

  
• Sound and relatively complete belief Hoare logic for statistical hypothesis testing programs.

  Yusuke Kawamoto 0001; Tetsuya Sato 0001; Kohei Suenaga

  Artif. Intell., Jan. 2024, Peer-reviewed, Last author

  
• Learning Nonlinear Hybrid Automata from Input-Output Time-Series Data.

  Amit Gurung; Masaki Waga; Kohei Suenaga

  ATVA (1), 2023

  
• Goal-Aware RSS for Complex Scenarios via Program Logic

  Ichiro Hasuo; Clovis Eberhart; James Haydon; Jérémy Dubut; Rose Bohrer; Tsutomu Kobayashi; Sasinee Pruekprasert; Xiao-Yi Zhang; Erik André Pallas; Akihisa Yamada; Kohei Suenaga; Fuyuki Ishikawa; Kenji Kamijo; Yoshiyuki Shinya; Takamasa Suetomi

  IEEE Transactions on Intelligent Vehicles, Apr. 2023, Peer-reviewed

  
• Probabilistic Black-Box Checking via Active MDP Learning

  Junya Shijubo; Masaki Waga; Kohei Suenaga

  ACM Transactions on Embedded Computing Systems, 31 Oct. 2023, Peer-reviewed, Last author

  
• Formalizing Statistical Causality via Modal Logic

  Yusuke Kawamoto; Tetsuya Sato; Kohei Suenaga

  JELIA 2023, Sep. 2023, Peer-reviewed, Last author

  
• BOREx: Bayesian-Optimization-Based Refinement of Saliency Map for Image- and Video-Classification Models.

  Atsushi Kikuchi; Kotaro Uchida; Masaki Waga; Kohei Suenaga

  ACCV (7), 2022

  
• Feature Attributionを用いたdlshogiの指し手の解釈可能性向上手法

  廣瀬 雄一; 和賀 正樹; 末永 幸平

  研究報告ゲーム情報学（GI）, Mar. 2023

  
• LLTZ: LLVM IR からスマートコントラクト記述言語 Michelson へのコンパイラ

  臼澤嘉; 末永幸平; 古瀬淳; 五十嵐淳

  第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023) 論文集, Mar. 2023, Peer-reviewed

  
• Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types.

  Yuki Nishida; Hiromasa Saito; Ran Chen; Akira Kawata; Jun Furuse; Kohei Suenaga; Atsushi Igarashi

  New Generation Computing, 2022, Peer-reviewed

  Access this paper :

  
• SCameleer: スマートコントラクト記述言語SCamlのための自動検証器

  服部 佑哉; 西田 雄気; 古瀬 淳; 末永 幸平; 五十嵐 淳

  日本ソフトウェア科学会 第39回大会講演論文集, Sep. 2022

  
• スマートコントラクト検証器Helmholtzのためのエラー原因提示手法

  小野 雄登; 西田 雄気; 古瀬 淳; 末永 幸平; 五十嵐 淳

  日本ソフトウェア科学会 第39回大会講演論文集, Sep. 2022

  
• Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption.

  Ryotaro Banno; Kotaro Matsuoka; Naoki Matsumoto; Song Bian; Masaki Waga; Kohei Suenaga

  CAV 2022, 2022, Peer-reviewed

  
• The Lattice-Theoretic Essence of Property Directed Reachability Analysis.

  Mayuko Kori; Natsuki Urabe; Shin-ya Katsumata; Kohei Suenaga; Ichiro Hasuo

  CAV 2022, 2022, Peer-reviewed

  
• Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types.

  Yuki Nishida 0001; Hiromasa Saito; Ran Chen; Akira Kawata; Jun Furuse; Kohei Suenaga; Atsushi Igarashi

  Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, 2021, Peer-reviewed

  Access this paper :

  
• Ordered Types for Stream Processing of Tree-Structured Data

  Sato Ryosuke; Suenaga Kohei; Kobayashi Naoki

  Information and Media Technologies, 2011

  
• 完全準同型暗号を用いた秘匿LTLオンラインモニタリング

  伴野 良太郎; 松岡 航太郎; 松本 直樹; Bian Song; 和賀 正樹; 末永 幸平

  コンピュータセキュリティシンポジウム 2021 (CSS 2021), Oct. 2021, Last author

  
• Formalizing Statistical Beliefs in Hypothesis Testing Using Program Logic.

  Yusuke Kawamoto; Tetsuya Sato; Kohei Suenaga

  Proceedings of the 18th International Conference on Principles of Knowledge Representation and Reasoning(KR), 2021, Peer-reviewed

  
• Efficient Black-Box Checking via Model Checking with Strengthened Specifications

  Junya Shijubo; Masaki Waga; Kohei Suenaga

  Runtime Verification - 21st International Conference(RV), 2021, Peer-reviewed, Last author

  
• Enhancing Loop-Invariant Synthesis via Reinforcement Learning.

  Takeshi Tsukada; Hiroshi Unno 0001; Taro Sekiyama; Kohei Suenaga

  CoRR, 2021

  
• Verification of a Merkle Patricia Tree Library Using F*

  Sota Sato; Ryotaro Banno; Jun Furuse; Kohei Suenaga; Atsushi Igarashi

  CoRR, 2021

  
• Control-data separation and logical condition propagation for efficient inference on probabilistic programs

  Ichiro Hasuo; Yuichiro Oyabu; Clovis Eberhart; Kohei Suenaga; Kenta Cho; Shin-ya Katsumata

  Journal of Logical and Algebraic Methods in Programming, Jan. 2024, Peer-reviewed

  
• スマートコントラクトのための Effectively Callback-Free 性の型に基づく静的検証

  齋藤 大聖; 西田 雄気; 五十嵐 淳; 末永 幸平

  PPL 2020, Mar. 2020, Peer-reviewed

  
• F*を用いたMerkle Patricia Treeライブラリの形式検証

  佐藤 聡太; 古瀬 淳; 末永 幸平; 五十嵐 淳

  PPL 2020, Mar. 2020, Peer-reviewed

  
• Visualizing Color-Wise Saliency of Black-Box Image Classification Models.

  Yuhki Hatakeyama; Hiroki Sakuma; Yoshinori Konishi; Kohei Suenaga

  Proceedings of ACCV 2020, 2020, Peer-reviewed

  
• Generalized Property-Directed Reachability for Hybrid Systems

  Kohei Suenaga; Takuya Ishizawa

  Verification, Model Checking, and Abstract Interpretation - 21st International Conference(VMCAI), 2020, Peer-reviewed

  
• A Contract Corpus for Recognizing Rights and Obligations.

  Ruka Funaki; Yusuke Nagata; Kohei Suenaga; Shinsuke Mori

  Proceedings of The 12th Language Resources and Evaluation Conference(LREC), 2020, Peer-reviewed

  
• ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs

  John Toman; Ren Siqi; Kohei Suenaga; Atsushi Igarashi; Naoki Kobayashi

  29th European Symposium on Programming (ESOP 2020), 2020, Peer-reviewed

  Access this paper :

  
• Automated Proof Synthesis for the Minimal Propositional Logic with Deep Neural Networks

  Taro Sekiyama; Kohei Suenaga

  APLAS 2018, 2018, Peer-reviewed

  
• A guess-and-assume approach to loop fusion for program verification.

  Akifumi Imanishi; Kohei Suenaga; Atsushi Igarashi

  PEPM 2018, 2018, Peer-reviewed

  
• MONAA: A Tool for Timed Pattern Matching with Automata-Based Acceleration.

  Masaki Waga; Ichiro Hasuo; Kohei Suenaga

  3rd Workshop on Monitoring and Testing of Cyber-Physical Systems, MT@CPSWeek 2018, Porto, Portugal, April 10, 2018, 2018, Peer-reviewed

  
• Generalized homogeneous polynomials for efficient template-based nonlinear invariant synthesis.

  Kensuke Kojima; Minoru Kinoshita; Kohei Suenaga

  Theor. Comput. Sci., 2018, Peer-reviewed

  
• A Nonstandard Functional Programming Language

  Hirofumi Nakamura; Kensuke Kojima; Kohei Suenaga; Atsushi Igarashi

  Programming Languages and Systems (APLAS 2017), 2017, Peer-reviewed

  
• Efficient Online Timed Pattern Matching by Automata-Based Skipping

  Masaki Waga; Ichiro Hasuo; Kohei Suenaga

  FORMATS 2017, 2017, Peer-reviewed

  
• Towards Proof Synthesis Guided by Neural Machine Translation for Intuitionistic Propositional Logic

  Taro Sekiyama; Akifumi Imanishi; Kohei Suenaga

  CoRR, 2017, Peer-reviewed

  
• An Extended Behavioral Type System for Memory-Leak Freedom

  Qi Tan; Kohei Suenaga; Atsushi Igarashi

  日本ソフトウェア科学会第33回大会論文集, Sep. 2016

  
• Generalized Homogeneous Polynomials for Efficient Template-Based Nonlinear Invariant Synthesis.

  Kensuke Kojima; Minoru Kinoshita; Kohei Suenaga

  STATIC ANALYSIS, (SAS 2016), 2016, Peer-reviewed

  
• Input Synthesis for Sampled Data Systems by Program Logic

  Takumi Akazaki; Ichiro Hasuo; Kohei Suenaga

  Proc. of the 4th Workshop on Hybrid Autonomous Systems (HAS 2014), 24 Jan. 2015, Peer-reviewed

  
• Validated Numerics Meets Reachability Analysis for CPS Design (NII Shonan Meeting 2015-14).

  Daisuke Ishii; Kohei Suenaga; Walid Taha

  NII Shonan Meet. Rep., 2015

  
• Automatic Memory Management Based on Program Transformation Using Ownership.

  Tatsuya Sonobe; Kohei Suenaga; Atsushi Igarashi

  Programming Languages and Systems - 12th Asian Symposium, APLAS 2014, Singapore, November 17-19, 2014, Proceedings, 2014, Peer-reviewed

  
• Hyperstream processing systems: Nonstandard modeling of continuous-time signals

  Kohei Suenaga; Hiroyoshi Sekine; Ichiro Hasuo

  Conference Record of the Annual ACM Symposium on Principles of Programming Languages, 2013, Peer-reviewed

  
• Type-based safe resource deallocation for shared-memory concurrency

  Kohei Suenaga; Ryota Fukuda; Atsushi Igarashi

  Proceedings of OOPSLA 2021, Oct. 2012, Peer-reviewed

  
• Exercises in Nonstandard Static Analysis of Hybrid Systems

  Ichiro Hasuo; Kohei Suenaga

  24th International Conference, CAV 2012, 2012, Peer-reviewed

  
• Programming with Infinitesimals: A WHILE-Language for Hybrid System Modeling

  Kohei Suenaga; Ichiro Hasuo

  Automata, Languages and Programming, ICALP, Pt II, 2011, Peer-reviewed

  
• RA-010 Ordered Types for Stream Processing of Tree-Structured Data

  Sato Ryosuke; Suenaga Kohei; Kobayashi Naoki

  情報科学技術フォーラム講演論文集, 20 Aug. 2009

  
• Fractional Ownerships for Safe Memory Deallocation

  Kohei Suenaga; Naoki Kobayashi

  7th Asian Symposium, APLAS 2009, 2009, Peer-reviewed

  
• Identifying Deadlock Errors by Type Error Slicing

  飯村 枝里; 小林 直樹; 末永 幸平

  情報処理学会論文誌プログラミング（PRO）, 26 Sep. 2008

  
• Type-Based Deadlock-Freedom Verification for Non-Block-Structured Lock Primitives and Mutable References

  Kohei Suenaga

  6th Asian Symposium, APLAS 2008, 2008, Peer-reviewed, Lead author

  
• Translation of tree-processing programs into stream-processing programs based on ordered linear type

  Koichi Kodama; Kohei Suenaga; Naoki Kobayashi

  J. Funct. Program., 2008, Peer-reviewed

  
• Type-based analysis of deadlock for a concurrent calculus with interrupts

  Kohei Suenaga; Naoki Kobayashi

  ESOP'07: Proceedings of the 16th European Symposium on Programming, 2007, Peer-reviewed

  
• Extension of type-based approach to generation of stream-processing programs by automatic insertion of buffering primitives

  Kohei Suenaga; Naoki Kobayashi; Akinori Yonezawa

  LOPSTR'05: Proceedings of the 15th international conference on Logic Based Program Synthesis and Transformation, 2006, Peer-reviewed

  
• Resource usage analysis for the pi-calculus

  N Kobayashi; K Suenaga; L Wischik

  7th International Conference, VMCAI 2006, 2006, Peer-reviewed

  
• Resource Usage Analysis for the Pi-Calculus

  Naoki Kobayashi; Kohei Suenaga; Lucian Wischik

  Logical Methods in Computer Science, 2006, Peer-reviewed

  
• The Interface Definition Language for Fail-Safe C

  K Suenaga; Y Oiwa; E Sumii; A Yonezawa

  SOFTWARE SECURITY - THEORIES AND SYSTEMS, 2004, Peer-reviewed

  
• Translation of tree-processing programs into stream-processing programs based on ordered linear type

  K Kodama; K Suenaga; N Kobayashi

  PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS, 2004, Peer-reviewed

  
• Fail-Safe Cのためのインターフェイス定義言語

  末永幸平; 大岩寛; 住井英二郎; 米澤明憲

  第5回プログラミングおよびプログラミング言語ワークショップ(PPL 2003)論文集, 2003, Peer-reviewed

  
• Formal Verification of CPS : A Nonstandard Analysis Approach

  HASUO Ichiro; SUENAGA Kohei

  Journal of The Society of Instrument and Control Engineers, 2014

  

Misc.

• Learning Heuristics for Template-based CEGIS of Loop Invariants with Reinforcement Learning

  Minchao Wu; Takeshi Tsukada; Hiroshi Unno; Taro Sekiyama; Kohei Suenaga

  16 Jul. 2021

  
• 昔のネタ帳から

  末永幸平

  コンピュータソフトウェア, Apr. 2022, Invited

  
• PLDI 2016 Report

  末永 幸平

  コンピュータソフトウェア = Computer software, Feb. 2017, Invited

  

Presentations

• Formal Verification and AI as a Black Box

  Kohei Suenaga

  「論理とAI」Online ワークショップ：UNESCO世界論理デー記念行事, 10 Jan. 2026, Invited

  
• Efficient Black-Box Checking with Specification-Guided Abstraction

  Tsubasa Matsumoto; Kazuki Watanabe; Kohei Suenaga; Masaki Waga

  EMSOFT 2025, Oct. 2025

  
• 画像分類モデルの解釈性向上のための明瞭なヒートマップの生成手法

  末永幸平

  第116回 産研テクノサロン, 14 Oct. 2025, Invited

  
• 制御フロー仕様から生成したペトリネットに基づくハードウェア誤動作検出手法

  田中知成; 上薗巧; 末永幸平; 橋本昌宜

  DAシンポジウム 2024, 28 Aug. 2024

  
• Learning nonlinear hybrid automata from input-output time-series data

  Amit Gurung; Masaki Waga; Kohei Suenaga

  ATVA 2023, Oct. 2023

  
• Probabilistic Black-Box Checking via Active MDP Learning

  Junya Shijubo; Masaki Waga; Kohei Suenaga

  EMSOFT 2023, Sep. 2023

  
• Formalizing Statistical Causality via Modal Logic

  Yusuke Kawamoto; Tetsuya Sato; Kohei Suenaga

  JELIA 2023, Sep. 2023

  
• Probabilistic Black-Box Checking via Active MDP Learning

  Junya Shijubo; Masaki Waga; Kohei Suenaga

  EMSOFT 2023, Sep. 2023

  
• Feature Attributionを用いたdlshogiの指し手の解釈可能性向上手法

  廣瀬 雄一; 和賀 正樹; 末永 幸平

  第49回ゲーム情報学研究発表会, 17 Mar. 2023

  
• SCameleer: スマートコントラクト記述言語SCamlのための自動検証器

  服部佑哉; 西田雄気; 古瀬淳; 末永幸平; 五十嵐淳

  第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023), 08 Mar. 2023

  
• LLTZ: LLVM IR からスマートコントラクト記述言語 Michelson へのコンパイラ

  臼澤嘉; 末永幸平; 古瀬淳; 五十嵐淳

  第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023), 07 Mar. 2023

  
• LLTZ: LLVM IR からスマートコントラクト記述言語 Michelson へのコンパイラ

  Yoshi Usuzawa; Kohei Suenaga; Jun Furuse; Atsushi Igarashi

  第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023), 06 Mar. 2023

  
• Java 検証器 Regnant の帰還

  Ryota Kobayashi; Atsushi Igarashi; Kohei Suenaga

  第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023), 06 Mar. 2023

  
• 並行命令型プログラミング言語のための所有権篩型システム

  Junya Hirashima; Atsushi Igarashi; Kohei Suenaga

  第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023), 06 Mar. 2023

  
• ゼロ知識証明を用いて真正性を保証する通信プロトコルのための篩型システム

  Zijian Zhao; Kohei Suenaga; Atsushi Igarashi

  第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023), 06 Mar. 2023

  
• Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types

  Kohei Suenaga

  US-Japan Seminar on Autonomy AI, Robotics, and Informatics, 11 Oct. 2022, Invited

  
• JST CREST 研究課題「AI 集約的サイバーフィジカルシステムの形式的解析設計手法」の概観と研究成果の紹介

  末永幸平

  2022年電子情報通信学会ソサイエティ大会企画セッション「 AI を含むサイバーフィジカルシステムの背景技術 〜信頼性向上を⽬指して〜」, 06 Sep. 2022, Invited

  
• SCameleer: スマートコントラクト記述言語SCamlのための自動検証器

  服部 佑哉; 西田 雄気; 古瀬 淳; 末永 幸平; 五十嵐 淳

  日本ソフトウェア科学会第39回大会, 02 Sep. 2022

  
• スマートコントラクト検証器Helmholtzのためのエラー原因提示手法

  小野 雄登; 西田 雄気; 古瀬 淳; 末永 幸平; 五十嵐 淳

  日本ソフトウェア科学会第39回大会, 01 Sep. 2022

  
• Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption

  Ryotaro Banno; Kotaro Matsuoka; Naoki Matsumoto; Song Bian; Masaki Waga; Kohei Suenaga

  CAV 2022, Aug. 2022

  
• The Lattice-Theoretic Essence of Property Directed Reachability Analysis

  Mayuko Kori; Natsuki Urabe; Shin-ya Katsumata; Kohei Suenaga; Ichiro Hasuo

  CAV 2022, Aug. 2022

  
• 物理情報システムに対するブラックボックス検査の構文的仕様強化による最適化

  四十坊純也; 和賀正樹; 末永幸平

  第23回プログラミングおよびプログラミング言語ワークショップ (PPL 2021), 10 Mar. 2021

  
• 暗号通貨向けストレージシステムにおけるデータ永続化処理の形式検証

  伴野良太郎; 佐藤聡太; 古瀬淳; 末永幸平; 五十嵐淳

  第23回プログラミングおよびプログラミング言語ワークショップ (PPL 2021), 09 Mar. 2021

  
• Visualizing Color-Wise Saliency of Black-Box Image Classification Models

  Yuhki Hatakeyama; Hiroki Sakuma; Yoshinori Konishi; Kohei Suenaga

  ACCV 2020

  
• ブラックボックス画像分類モデルの否定的判断根拠と色情報根拠の可視化

  畠山雄気; 佐久間宏樹; 小西嘉典; 末永幸平

  MIRU 2020

  
• F*を用いたMerkle Patricia Treeライブラリの形式検証

  佐藤 聡太; 古瀬 淳; 末永 幸平; 五十嵐 淳

  PPL 2020

  
• スマートコントラクトのための Effectively Callback-Free 性の型に基づく静的検証

  齋藤 大聖; 西田 雄気; 五十嵐 淳; 末永 幸平

  PPL 2020

  
• Generalized Property-Directed Reachability for Hybrid Systems

  Kohei Suenaga; Takuya Ishizawa

  VMCAI 2020, 19 Jan. 2020

  
• Automated proof synthesis for propositional logic using deep learning

  Kohei Suenaga

  5th France-Japan Cybersecurity workshop, 23 Apr. 2019, Invited

  
• 日本語契約書の一般的な構造定義に向けて

  舟木類佳; 末永幸平; 森信介

  13 Mar. 2019

  
• Automated Proof Synthesis for the Minimal Propositional Logic with Deep Neural Networks

  Taro Sekiyama; Kohei Suenaga

  APLAS 2018, 03 Dec. 2018

  
• Property-Directed Reachability for Hybrid Systems with Differential Dynamic Logic Predicates

  Takuya Ishizawa; Kohei Suenaga

  APLAS 2018 Student Research Competition, 02 Dec. 2018

  
• ニューラルネットワークによるフォトニック結晶格子点構造の3次元モデリングの検討

  田上 智基; 北村 恭子; 末永 幸平; 石崎 賢司; 野田 進

  第65回応用物理学会春季学術講演会, 20 Mar. 2018

  
• Towards Proof Synthesis by Neural Machine Translation

  Taro Sekiyama; Akifumi Imanishi; Kohei Suenaga

  Off the Beaten Track 2018 (OBT 2018), 13 Jan. 2018

  
• A Guess-and-Assume Approach to Loop Fusion for Program Verification

  Akifumi Imanishi; Kohei Suenaga; Atsushi Igarashi

  PEPM 2018, 07 Jan. 2018

  
• 超準プログラミング言語を用いたハイブリッドシステムのモデリングと検証

  末永 幸平

  第9回 暗号及び情報セキュリティと数学の相関ワークショップ (CRISMATH 2017), 22 Dec. 2017, Invited

  
• A Nonstandard Functional Programming Language

  Hirofumi Nakamura; Kensuke Kojima; Kohei Suenaga; Atsushi Igarashi

  APLAS 2017, 27 Nov. 2017

  
• Sharper and Simpler Nonlinear Interpolants for Program Verification

  Takamasa Okudono; Yuki Nishida; Kensuke Kojima; Kohei Suenaga; Kengo Kido; Ichiro Hasuo

  APLAS 2017, 27 Nov. 2017

  
• Efficient Online Timed Pattern Matching by Automata-Based Skipping

  Masaki Waga; Ichiro Hasuo; Kohei Suenaga

  15th International Conference on Formal Modelling and Analysis of Timed Systems, 05 Sep. 2017

  
• Sharper and Simpler Nonlinear Interpolants for Program Verification

  Takamasa Okudono; Yuki Nishida; Kensuke Kojima; Kohei Suenaga; Kengo Kido; Ichiro Hasuo

  Workshop on Formal Approaches to Explainable VERification (FEVER 2017), 23 Jul. 2017

  
• 超準関数型プログラミング言語NSF

  中村 博文; 末永 幸平; 五十嵐 淳; 小島 健介

  第19回プログラミングおよびプログラミング言語ワークショップ（PPL2017）, 08 Mar. 2017

  
• 深層学習によるプログラム生成の高速化

  今西 諒文; 関山 太朗; 村主 崇行; 末永 幸平

  第19回プログラミングおよびプログラミング言語ワークショップ（PPL2017）, 08 Mar. 2017

  
• 無限状態システムのHFLモデル検査のための型に基づく手法

  今井 雄毅; 小林 直樹; 佐藤 亮介; 末永 幸平; 塚田 武志

  第19回プログラミングおよびプログラミング言語ワークショップ（PPL2017）, 08 Mar. 2017

  
• Generalized Homogeneous Polynomials for Efficient Template-Based Nonlinear Invariant Synthesis

  Kensuke Kojima; Minoru Kinoshita; Kohei Suenaga

  第19回プログラミングおよびプログラミング言語ワークショップ（PPL2017）, 08 Mar. 2017

  
• 超準解析を用いたハイブリッドシステム検証手法

  末永 幸平

  統計数理解析研究所シンポジウム --- 工学と現代数学の接点を求めて, 20 Dec. 2016, Invited

  
• Generalized Homogeneous Polynomials for Efficient Template-Based Nonlinear Invariant Synthesis

  Kohei Suenaga

  SAS 2016, 08 Sep. 2016

  
• An Extended Behavioral Type System for Memory-Leak Freedom

  Qi Tan; Kohei Suenaga; Atsushi Igarashi

  日本ソフトウェア科学会 第33回大会講演論文集, 07 Sep. 2016

  
• ソフトウェアのための自動形式検証ツール

  末永 幸平

  ET/IoT 総合技術展 関西（ETWest 2016）, 07 Jul. 2016

  
• Formal verification of software, continuous, and hybrid systems -- Or: How do we verify our program is correct?

  Kohei Suenaga

  Machine Learning Summer School 2015, 27 Aug. 2015

  
• Nonstandard Analysis Meets Programming Language Theory

  Kohei Suenaga

  Twelfth International Conference on Computability and Complexity in Analysis, 13 Jul. 2015, Invited

  
• Automatic Synthesis of Combiners in the MapReduce Framework

  Minoru Kinoshita; Kohei Suenaga; Atsushi Igarashi

  24th International Symposium on Logic-Based Program Synthesis and Transformation, 09 Sep. 2014

  
• Type-Based Safe Resource Deallocation for Shared-Memory Concurrency

  末永 幸平

  日本ソフトウェア科学会第30回大会特別招待講演, 12 Sep. 2013, Invited

  
• 形式検証手法は無限小プログラミングを使えばハイブリッドシステムにもそのまま使える

  末永 幸平

  日本ソフトウェア科学会第30回大会Future Technology Design (FTD) 2013, 11 Sep. 2013, Invited

  
• Simulink blocks as stream processing ─ An approach from nonstandard analysis (Preliminary Report)

  Hiroyoshi Sekine; Kohei Suenaga; Ichiro Hasuo

  Fifth International Workshop on Numerical Software Verification (NSV 2012), 07 Jul. 2012

  
• 京都大学 Teen Racketeer 養成コース

  五十嵐 淳; 中澤 巧爾; 馬谷 誠二; 関山 太朗; 花田 裕一朗; 大元 武; 宮本 洋平; 末永 幸平

  第17回プログラミングおよびプログラミング言語ワークショップ, 05 Mar. 2015

  
• The Lattice-Theoretic Essence of Property Directed Reachability Analysis

  Mayuko Kori; Natsuki Urabe; Shin-ya Katsumata; Kohei Suenaga; Ichiro Hasuo

  16th IFIP WG 1.3 International Workshop on Coalgebraic Methods in Computer Science (CMCS 2022), 03 Apr. 2022

  
• Regnant: 分割可能所有権と篩型を用いた Java 検証器

  小林 亮太; John Toman; 五十嵐 淳; 末永 幸平

  第24回プログラミングおよびプログラミング言語ワークショップ（PPL 2022）, 08 Mar. 2022

  
• Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types

  Yuki Nishida; Hiromasa Saito; Ran Chen; Akira Kawata; Jun Furuse; Kohei Suenaga; Atsushi Igarashi

  第24回プログラミングおよびプログラミング言語ワークショップ（PPL 2022）, 06 Mar. 2022

  

Books and Other Publications

• プログラミング言語の形式的意味論入門

  末永 幸平; 勝股 審也; 中澤 巧爾; 西村 進; 前田 敦司, Joint translation, G.ウィンスケル

  丸善出版, 30 Jan. 2023

  Find Kyoto University's collection of books :

  
• Encyclopedia of theoretical computer science

  徳山, 豪; 小林, 直樹; 岩間, 一雄; 渡辺, 治; 今井, 浩; 南出, 靖彦; 五十嵐, 淳; 長谷川, 真人, Section 8.3 "Program verification based on type systems"

  朝倉書店, Jan. 2022

  Find Kyoto University's collection of books :

  

Industrial Property Rights

• 特許7671514, 特表2022-034637, 特願2022-542524, Document Processing Program, Information Processing Apparatus, and Document Processing Method

  Ruka Funaki; Shinsuke Mori; Kohei Suenaga; Yusuke Nagata

  
• US 12,182,492 B2, US 2023/0186012 A1, US 18/107,639, Document Processing Method, and Information Processing Device

  Ruka Funaki; Shinsuke Mori; Kohei Suenaga; Yusuke Nagata

  
• 特開2023-069054, 特願2021-180647, 情報処理装置、情報処理方法および情報処理プログラム

  末永 幸平; 菊池 淳; 和賀 正樹

  
• 特許第6910228号, 特開2019-020966, 特願2017-137949, 自動証明装置、及びプログラム

  蓮尾 一郎; 奥殿 貴仁; 木戸 肩吾; 末永 幸平; 小島 健介; 西田 雄気

  
• 特許第6632058号, 特開2017-138679, 特願2016-017441, 不変条件生成装置、コンピュータプログラム、不変条件生成方法、プログラムコード製造方法

  末永 幸平; 樹下 稔; 小島 健介

  
• 特許第6622098号, 特開2017-138677, 特願2016-017419, 不変条件生成装置、コンピュータプログラム、不変条件生成方法、プログラムコード製造方法

  末永 幸平; 樹下 稔; 小島 健介

  
• 特開2019-113997, 特願2017-246154, プログラム検証装置、プログラム検証方法、プログラム検証のためのコンピュータプログラム、プログラム変換器、プログラム変換方法、プログラム変換のためのコンピュータプログラム、プログラム製造方法、及び検証用プログラム

  末永 幸平; 今西 諒文; 五十嵐 淳

  
• 特開2013-003897, 特願2011-135201, ハイブリッドシステムの検証方法、検証装置、及び検証コンピュータプログラム、並びに、ハイブリッドシステムのモデル変換方法、変換装置、及び変換コンピュータプログラム

  末永 幸平; 蓮尾 一郎

  
• 特開2012-027685, 特願2010-165620, 情報管理システム、方法及びプログラム

  中村 宏明; 宮下 尚; 末永 幸平

  
• 特願2024-007664, ブラックボックスシステムのテストのためのコンピュータ実装方法及びコンピュータシステム

  Amit Gurung; Masaki Waga; Kohei Suenaga

  
• 特願2021-180647, 情報処理装置、情報処理方法および情報処理プログラム

  菊池淳; 和賀正樹; 末永幸平

  
• PCT/JP2018/044029, プログラム検証装置、プログラム検証方法、プログラム検証のためのコンピュータプログラム、 プログラム変換器、プログラム変換方 法、プログラム変換のためのコンピュータプログラム、 プログラム製造方法、及び検証用プログラム

  末永 幸平; 今西 諒文; 五十嵐 淳

  
• 特許6632058, 特開2017-138679, 特願2016-017441, 不変条件生成装置、コンピュータプログラム、不変条件生成方法、プログラムコード製造方法

  末永 幸平; 樹下 稔; 小島 健介

  
• PCT/JP2017/003295, 不変条件生成装置、コンピュータプログラム、不変条件生成方法、プログラムコード製造方法

  樹下稔; 小島健介; 末永幸平

  
• 特開2015-194917, 特願2014-072623, 制御入力値生成装置、制御入力値生成方法、および、プログラム

  蓮尾 一郎; 赤崎 拓未; 末永 幸平

  

Awards

• Mar. 2007

  日本ソフトウェア科学会プログラミング論研究会, PPL 2007 発表賞
• Mar. 2009

  日本ソフトウェア科学会プログラミング論研究会, PPL 2009 発表賞
• Mar. 2012

  日本ソフトウェア科学会プログラミング論研究会, PPL 2012 発表賞
• Jun. 2012

  情報処理学会, Journal of Information Processing Outstanding Paper Award
• Sep. 2013

  京都大学, 京都大学学際研究着想コンテスト優秀賞

Media Coverage

• “あいまい”検索システム「SoftMatcha 2」 東大や京大、Sakana AIなどが開発 巨大化するAI学習データを高速検索

  ITmedia AI+, 19 Feb. 2026, Internet

  

External funds: Kakenhi

• Research on software contracts for highly interoperable software modules

  Grant-in-Aid for Scientific Research (A)

  Medium-sized Section 60:Information science, computer engineering, and related fields

  Kyoto University

  五十嵐 淳

  From 01 Apr. 2020, To 31 Mar. 2025, Granted

  プログラミング言語;プログラム検証;相互運用性;ソフトウェア契約;ソフトウエア契約

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-20H00582/
• Automated Theorem Proving with Machine Learning for Automating Mathematics

  Grant-in-Aid for Challenging Research (Exploratory)

  Medium-sized Section 60:Information science, computer engineering, and related fields

  Kyoto University

  Kohei Suenaga

  From 28 Jun. 2019, To 31 Mar. 2022, Project Closed

  強化学習;自動証明;制約付きホーン節;機械学習;プログラム検証;定理証明;ホーン節ソルバ;人工知能;深層学習

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-19K22842/
• Enhancement of Formal Verification for IoT Systems

  Grant-in-Aid for Scientific Research (B)

  Basic Section 60050:Software-related

  Kyoto University

  Kohei Suenaga

  From 01 Apr. 2019, To 31 Mar. 2024, Project Closed

  ハイブリッドシステム;モデル検査;プログラム検証;形式検証;ブラックボックス検査;モニタリング;PDR;IoT;強化学習;機械学習;形式手法

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-19H04084/
• Supporting Manufacturing by Category Theory and Mathematical Logic: Transfer of Software Science to Systems Engineering

  Grant-in-Aid for Scientific Research (B)

  National Institute of Informatics;The University of Tokyo

  Ichiro Hasuo

  From 10 Jul. 2015, To 31 Mar. 2020, Project Closed

  物理情報システム;形式検証;テスト;ハイブリッドシステム;数理論理学;統計的機械学習;圏論;プログラム理論;モデルベース開発;不動点論理;システム工学;応用数学

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-15KT0012/
• Forma verification of hybrid systems based on the infinitesimal programming

  Grant-in-Aid for Young Scientists (B)

  Kyoto University

  Kohei Suenaga

  From 01 Apr. 2013, To 31 Mar. 2016, Project Closed

  ハイブリッドシステム;プログラム検証;不変条件;無限小プログラミング;超準解析;次元解析;非線形不変条件;システム検証;形式手法;形式検証;プログラミング言語;プログラミング言語理論;プログラム意味論;プログラム理論

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-25730040/
• Theory of Higher-Order Typed Programs based Software Contracts

  Grant-in-Aid for Scientific Research (B)

  Kyoto University

  Atsushi Igarashi

  From 01 Apr. 2013, To 31 Mar. 2017, Project Closed

  プログラミング言語;ソフトウェア契約;計算効果;プログラム検証;トレース意味論;代入;限定継続;ゲーム意味論;shift/reset

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-25280024/
• 無限小プログラミングによるハイブリッドシステムの形式検証手法

  Grant-in-Aid for Research Activity Start-up

  Kyoto University

  末永 幸平

  From 31 Aug. 2012, To 31 Mar. 2014, Declined

  ハイブリッドシステム;超準解析;型システム;静的検証;形式手法;プログラミング言語;ホーア論理;無限小プログラミング

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-24800035/
• 機械学習技術による高速な演繹的推論エンジンの開発

  Grant-in-Aid for Scientific Research (B)

  Basic Section 60050:Software-related

  Chiba University

  塚田 武志

  From 01 Apr. 2022, To 31 Mar. 2027, Granted

  演繹的推論;機械学習;定理自動証明;CHCソルバ;プログラム検証;システム検証

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-22H03564/
• Formal verification methods for trustworthy statistics

  Grant-in-Aid for Scientific Research (B)

  Basic Section 60050:Software-related

  National Institute of Advanced Industrial Science and Technology

  川本 裕輔

  From 01 Apr. 2024, To 31 Mar. 2027, Granted

  形式手法;プログラム検証;自動検証;統計の信頼性;仮説検定;統計

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-24K02924/
• Development of foundational technology for reliability assessment of next-generation integrated systems to overcome cosmic ray-induced malfunctions

  Grant-in-Aid for Scientific Research (S)

  Broad Section J

  Kyoto University

  橋本 昌宜

  From 01 Apr. 2024, To 31 Mar. 2029, Granted

  ソフトエラー;宇宙線;超伝導回路;集積回路;信頼性

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-24H00073/
• 機械学習技術による高速な演繹的推論エンジンの開発

  Grant-in-Aid for Scientific Research (B)

  Basic Section 60050:Software-related

  Chiba University

  塚田 武志

  From 01 Apr. 2024, To 31 Mar. 2027, Granted

  演繹的推論;機械学習;定理自動証明;プログラム検証;CHC ソルバ;システム検証;CHCソルバ

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-23K24820/
• AIを含むソフトウェアのための形式検証手法

  Grant-in-Aid for Scientific Research (A)

  Medium-sized Section 60:Information science, computer engineering, and related fields

  Kyoto University

  末永 幸平

  From 01 Apr. 2025, To 31 Mar. 2030, Granted

  形式検証;人工知能;ソフトウェア

  https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-25H01113/

External funds: others

• 輻射を対象とした次世代熱制御材料の研究開発

  国立研究開発法人新エネルギー・産業技術総合開発機構, 官民による若手研究者発掘支援事業／共同研究フェーズ

  From Apr. 2021, To Mar. 2026

  坂本雅典

  末永幸平;Daniel Packwood

  研究分担者
• Formal methods for hybrid systems based on the theory of nonstandard programming langauges

  JST さきがけ

  From 01 Oct. 2015, To 31 Mar. 2019

  末永幸平
• CyPhAI: Formal Analysis and Design of AI-intenstive Cyber-PHysical SYstems

  JST CREST

  From 01 Nov. 2020, To 31 Mar. 2025

  末永幸平

Education

Teaching subject(s)

• From 01 Apr. 2026, To 31 Mar. 2027

  Mathematics in Practice for Computer Science

  9131, Spring, Faculty of Engineering, 2
• From 01 Apr. 2026, To 31 Mar. 2027

  Implementation of Programming Languages

  9128, Spring, Faculty of Engineering, 2
• From 01 Apr. 2026, To 31 Mar. 2027

  Information and Business

  9108, Spring, Faculty of Engineering, 2
• From 01 Apr. 2026, To 31 Mar. 2027

  Formal Semantics of Computer Programs

  3620, Spring, Graduate School of Informatics, 2
• From 01 Apr. 2026, To 31 Mar. 2027

  System Verification

  3666, Fall, Graduate School of Informatics, 2
• From 01 Apr. 2026, To 31 Mar. 2027

  Computer Science Laboratory and Exercise 3

  9084, Spring, Faculty of Engineering, 4
• From 01 Apr. 2025, To 31 Mar. 2026

  Computer Science Laboratory and Exercise 1

  9138, Spring, Faculty of Engineering, 2
• From 01 Apr. 2025, To 31 Mar. 2026

  Implementation of Programming Languages

  9128, Spring, Faculty of Engineering, 2
• From 01 Apr. 2025, To 31 Mar. 2026

  Information and Business

  9108, Spring, Faculty of Engineering, 2
• From 01 Apr. 2025, To 31 Mar. 2026

  Computer Science Laboratory and Exercise 2

  9022, Fall, Faculty of Engineering, 2
• From 01 Apr. 2025, To 31 Mar. 2026

  Formal Semantics of Computer Programs

  3620, Spring, Graduate School of Informatics, 2
• From 01 Apr. 2025, To 31 Mar. 2026

  System Verification

  3666, Fall, Graduate School of Informatics, 2
• From 01 Apr. 2025, To 31 Mar. 2026

  Computer Science Laboratory and Exercise 4

  9039, Fall, Faculty of Engineering, 3
• From 01 Apr. 2025, To 31 Mar. 2026

  Computer Science Laboratory and Exercise 3

  9084, Spring, Faculty of Engineering, 4
• From 01 Apr. 2024, To 31 Mar. 2025

  Implementation of Programming Languages

  9128, Spring, Faculty of Engineering, 2
• From 01 Apr. 2024, To 31 Mar. 2025

  System Verification

  3666, Fall, Graduate School of Informatics, 2
• From 01 Apr. 2024, To 31 Mar. 2025

  Formal Semantics of Computer Programs

  3620, Spring, Graduate School of Informatics, 2
• From 01 Apr. 2024, To 31 Mar. 2025

  Computer Science Laboratory and Exercise 3

  9084, Spring, Faculty of Engineering, 4
• From 01 Apr. 2023, To 31 Mar. 2024

  Implementation of Programming Languages

  9128, Spring, Faculty of Engineering, 2
• From 01 Apr. 2023, To 31 Mar. 2024

  System Verification

  3666, Fall, Graduate School of Informatics, 2
• From 01 Apr. 2023, To 31 Mar. 2024

  Formal Semantics of Computer Programs

  3620, Spring, Graduate School of Informatics, 2
• From 01 Apr. 2023, To 31 Mar. 2024

  Computer Science Laboratory and Exercise 3

  9084, Spring, Faculty of Engineering, 4
• From 01 Apr. 2022, To 31 Mar. 2023

  Formal Semantics of Computer Programs

  3620, Spring, Graduate School of Informatics, 2
• From 01 Apr. 2022, To 31 Mar. 2023

  Computer Science Laboratory and Exercise 2

  9022, Fall, Faculty of Engineering, 2
• From 01 Apr. 2022, To 31 Mar. 2023

  System Verification

  3666, Fall, Graduate School of Informatics, 2
• From 01 Apr. 2022, To 31 Mar. 2023

  Computer Science Laboratory and Exercise 1

  9138, Spring, Faculty of Engineering, 2
• From 01 Apr. 2022, To 31 Mar. 2023

  Computer Science Laboratory and Exercise 3

  9084, Spring, Faculty of Engineering, 4
• From 01 Apr. 2022, To 31 Mar. 2023

  Computer Science Laboratory and Exercise 4

  9039, Fall, Faculty of Engineering, 3
• From 01 Apr. 2022, To 31 Mar. 2023

  Implementation of Programming Languages

  9128, Spring, Faculty of Engineering, 2
• From Apr. 2013, To Mar. 2014

  Computer Science Laboratory and Exercise 4

  Fall, 工学部
• From Apr. 2014, To Mar. 2015

  Computer Science Laboratory and Exercise 1

  Spring, 工学部
• From Apr. 2014, To Mar. 2015

  Computer Science Laboratory and Exercise 4

  Fall, 工学部
• From Apr. 2014, To Mar. 2015

  Compilers

  Fall, 工学部
• From Apr. 2014, To Mar. 2015

  Formal Semantics of Computer Programs

  Spring, 情報学研究科
• From Apr. 2014, To Mar. 2015

  Parallel and Distributed Systems

  Fall, 情報学研究科
• From Apr. 2014, To Mar. 2015

  Seminar on Computer Engineering, Advanced

  Year-long, 情報学研究科
• From Apr. 2014, To Mar. 2015

  Advanced Study in Communications and Computer Engineering II

  Year-long, 情報学研究科
• From Apr. 2014, To Mar. 2015

  Advanced Study in Communications and Computer Engineering I

  Year-long, 情報学研究科
• From Apr. 2015, To Mar. 2016

  Advanced Study in Communications and Computer Engineering I

  Year-long, 情報学研究科
• From Apr. 2015, To Mar. 2016

  Advanced Study in Communications and Computer Engineering II

  Year-long, 情報学研究科
• From Apr. 2015, To Mar. 2016

  Compilers

  Fall, 工学部
• From Apr. 2015, To Mar. 2016

  Parallel and Distributed Systems

  Fall, 情報学研究科
• From Apr. 2015, To Mar. 2016

  Learning a functional programming language by game creating

  Spring, 全学共通科目
• From Apr. 2015, To Mar. 2016

  Seminar on Computer Engineering, Advanced

  Year-long, 情報学研究科
• From Apr. 2015, To Mar. 2016

  Formal Semantics of Computer Programs

  Spring, 情報学研究科
• From Apr. 2015, To Mar. 2016

  Computer Science Laboratory and Exercise 1

  Spring, 工学部
• From Apr. 2015, To Mar. 2016

  Computer Science Laboratory and Exercise 2

  Fall, 工学部
• From Apr. 2015, To Mar. 2016

  Computer Science Laboratory and Exercise 3

  Spring, 工学部
• From Apr. 2015, To Mar. 2016

  Computer Science Laboratory and Exercise 4

  Fall, 工学部
• From Apr. 2015, To Mar. 2016

  Advanced Study in Communications and Computer Engineering II

  Fall, 情報学研究科
• From Apr. 2015, To Mar. 2016

  Advanced Study in Communications and Computer Engineering II

  Year-long, 情報学研究科
• From Apr. 2015, To Mar. 2016

  Advanced Study in Communications and Computer Engineering I

  Year-long, 情報学研究科
• From Apr. 2016, To Mar. 2017

  Advanced Study in Communications and Computer Engineering I

  Year-long, 情報学研究科
• From Apr. 2016, To Mar. 2017

  Advanced Study in Communications and Computer Engineering II

  Year-long, 情報学研究科
• From Apr. 2016, To Mar. 2017

  ILAS Seminar

  Spring, 全学共通科目
• From Apr. 2016, To Mar. 2017

  Parallel and Distributed Systems

  Fall, 情報学研究科
• From Apr. 2016, To Mar. 2017

  Seminar on Computer Engineering, Advanced

  Year-long, 情報学研究科
• From Apr. 2016, To Mar. 2017

  Formal Semantics of Computer Programs

  Spring, 情報学研究科
• From Apr. 2016, To Mar. 2017

  Computer Science Laboratory and Exercise 4

  Fall, 工学部
• From Apr. 2016, To Mar. 2017

  Mathematics in Practice for Computer Science

  Spring, 工学部
• From Apr. 2016, To Mar. 2017

  Advanced Study in Communications and Computer Engineering II

  Spring, 情報学研究科
• From Apr. 2016, To Mar. 2017

  Advanced Study in Communications and Computer Engineering II

  Year-long, 情報学研究科
• From Apr. 2016, To Mar. 2017

  Advanced Study in Communications and Computer Engineering I

  Year-long, 情報学研究科
• From Apr. 2017, To Mar. 2018

  Advanced Study in Communications and Computer Engineering I

  Year-long, 情報学研究科
• From Apr. 2017, To Mar. 2018

  Advanced Study in Communications and Computer Engineering II

  Year-long, 情報学研究科
• From Apr. 2017, To Mar. 2018

  Parallel and Distributed Systems

  Fall, 情報学研究科
• From Apr. 2017, To Mar. 2018

  Seminar on Computer Engineering, Advanced

  Year-long, 情報学研究科
• From Apr. 2017, To Mar. 2018

  Formal Semantics of Computer Programs

  Spring, 情報学研究科
• From Apr. 2017, To Mar. 2018

  Implementation of Programming Languages

  Spring, 工学部
• From Apr. 2017, To Mar. 2018

  Computer Science Laboratory and Exercise 3

  Spring, 工学部
• From Apr. 2017, To Mar. 2018

  Mathematics in Practice for Computer Science

  Spring, 工学部
• From Apr. 2017, To Mar. 2018

  Advanced Study in Communications and Computer Engineering II

  Spring, 情報学研究科
• From Apr. 2017, To Mar. 2018

  Advanced Study in Communications and Computer Engineering II

  Year-long, 情報学研究科
• From Apr. 2017, To Mar. 2018

  Advanced Study in Communications and Computer Engineering I

  Year-long, 情報学研究科
• From Apr. 2018, To Mar. 2019

  Parallel and Distributed Systems

  Fall, 情報学研究科
• From Apr. 2018, To Mar. 2019

  Information and Business

  Spring, 工学部
• From Apr. 2018, To Mar. 2019

  Formal Semantics of Computer Programs

  Spring, 情報学研究科
• From Apr. 2018, To Mar. 2019

  Implementation of Programming Languages

  Spring, 工学部
• From Apr. 2018, To Mar. 2019

  Computer Science Laboratory and Exercise 3

  Spring, 工学部
• From Apr. 2018, To Mar. 2019

  Mathematics in Practice for Computer Science

  Spring, 工学部
• From Apr. 2019, To Mar. 2020

  Parallel and Distributed Systems

  Spring, 情報学研究科
• From Apr. 2019, To Mar. 2020

  Formal Semantics of Computer Programs

  Spring, 情報学研究科
• From Apr. 2019, To Mar. 2020

  Implementation of Programming Languages

  Spring, 工学部
• From Apr. 2019, To Mar. 2020

  Computer Science Laboratory and Exercise 3

  Spring, 工学部
• From Apr. 2019, To Mar. 2020

  Mathematics in Practice for Computer Science

  Spring, 工学部
• From Apr. 2020, To Mar. 2021

  Parallel and Distributed Systems

  Fall, 情報学研究科
• From Apr. 2020, To Mar. 2021

  Formal Semantics of Computer Programs

  Spring, 情報学研究科
• From Apr. 2020, To Mar. 2021

  Implementation of Programming Languages

  Spring, 工学部
• From Apr. 2020, To Mar. 2021

  Computer Science Laboratory and Exercise 3

  Spring, 工学部
• From Apr. 2020, To Mar. 2021

  Mathematics in Practice for Computer Science

  Spring, 工学部
• From Apr. 2021, To Mar. 2022

  Formal Semantics of Computer Programs

  Spring, 情報学研究科
• From Apr. 2021, To Mar. 2022

  System Verification

  Fall, 情報学研究科
• From Apr. 2021, To Mar. 2022

  Implementation of Programming Languages

  Spring, 工学部
• From Apr. 2021, To Mar. 2022

  Computer Science Laboratory and Exercise 3

  Spring, 工学部

Student achievements: Awards

• 第49回GI研究発表会優秀研究賞

  Yuichi Hirose, 情報処理学会ゲーム情報学研究会, May 2023

Administration

Faculty management (title, position)

• From 01 Apr. 2025, To 31 Mar. 2026

  情報セキュリティ委員会技術責任者
• From 01 Apr. 2025, To 31 Mar. 2027

  計算機小委員会 委員
• From 01 Apr. 2025, To 31 Mar. 2027

  情報セキュリティ作業委員会 委員
• From 01 Apr. 2021, To 31 Mar. 2027

  情報通信システム委員会 委員
• From 01 Apr. 2015, To 31 Mar. 2017

  情報セキュリティ作業委員会委員
• From 01 Apr. 2015, To 31 Mar. 2017

  計算機小委員会委員
• From 01 Apr. 2015, To 31 Mar. 2016

  ハラスメント窓口相談員
• From 01 Apr. 2016, To 31 Mar. 2017

  図書ＷＧ委員
• From 01 Apr. 2017, To 31 Mar. 2018

  情報セキュリティ作業委員会委員
• From 01 Apr. 2017, To 31 Mar. 2018

  計算機小委員会委員
• From 01 Apr. 2017, To 31 Mar. 2018

  図書WG委員
• From 01 Apr. 2018, To 31 Mar. 2019

  情報セキュリティ委員会委員（情報セキュリティ副技術責任者）
• From 01 Apr. 2018, To 31 Mar. 2019

  情報セキュリティ作業委員会委員
• From 01 Apr. 2018, To 31 Mar. 2019

  計算機小委員会委員
• From 01 Apr. 2020, To 31 Mar. 2022

  図書WG
• From 01 Apr. 2021, To 31 Mar. 2022

  連携推進WG委員

Academic, Social Contribution

Committee Memberships

• DSW 2026 プログラム委員
• FSTTCS 2026 プログラム委員
• From 2025, To 2026

  PPL 2026 プログラム委員
• VMCAI 2026 プログラム委員
• From Apr. 2025

  MLSE 2025 プログラム委員
• From Apr. 2025

  DSW 2025 プログラム委員
• プログラム委員長, 第8回機械学習工学研究会（MLSE夏合宿2024）
• Program committee member, ATVA 2024
• From Oct. 2022, To Sep. 2023

  日本ソフトウェア科学会第40回大会プログラム委員長, 日本ソフトウェア科学会
• From Apr. 2019, To Mar. 2023

  運営委員, 日本ソフトウェア科学会プログラミング論研究会
• From Apr. 2017, To May 2021

  支部委員, 情報処理学会関西支部
• From Jul. 2013, To Present

  専門調査員, 文部科学省科学技術政策研究所科学技術動向研究センター
• From Feb. 2012, To Present

  若手研究者の会, 情報処理学会
• From Oct. 2019, To Apr. 2020

  5th Workshop on Monitoring and Testing of Cyber-Physical Systems (MT-CPS 2020) プログラム共同委員長
• From Mar. 2018, To Mar. 2019

  PPL 2019 プログラム共同委員長
• From Apr. 2015, To Mar. 2019

  運営委員, 情報処理学会プログラミング研究会
• From Mar. 2015, To Mar. 2017

  幹事, 情報処理学会関西支部
• FLOPS 2020 プログラム委員
• PEPM 2018 プログラム委員
• PPL 2017 プログラム委員
• APLAS 2015 プログラム委員
• 実行委員, 第77回情報処理学会大会
• プログラム委員, ICTAC 2015
• プログラム委員, HSCC 2015
• プログラム委員, ACSI 2015
• 組織委員, PPL 2015
• 実行委員長, PPL 2014
• プログラム委員, SACSIS 2013
• プログラム委員, PEPM 2012
• MLSE 2020 プログラム委員
• From May 2021, To Jan. 2022

  POPL 2022 プログラム委員

Academic Contribution

• 2022年電子情報通信学会ソサイエティ大会企画セッション「 AI を含むサイバーフィジカルシステムの背景技術 〜信頼性向上を⽬指して〜」

  Planning, management, etc., Panel moderator

  電子情報通信学会, From 06 Sep. 2022, To 06 Sep. 2022

  

Social Contribution

• 研究発表会審査員

  Other

  鹿児島県立加治木高校 総合的な探究の時間(龍門学), From 15 Jan. 2025

  
• 巨人の肩の上に立つためのはしごを作るための大工道具

  Lecturer

  宮崎西高等学校, 理文クラス講演会, From 25 Oct. 2021

  
• PPL Summer School 2019 Organizer

  Host, Logistic support

  JSSST PPL, PPL Summer School 2019 "Block Chain and Formal Verification", From 26 Aug. 2019, To 26 Aug. 2019

  
• プログラムが正しく動くことを「証明」せよ

  Lecturer

  九州大学マス・フォア・インダストリ研究所・国立研究開発法人科学技術振興機構 (JST), 第29回JST数学キャラバン 拡がりゆく数学 in 福岡, From 15 Dec. 2018

  
• プログラムが正しく動くことを「証明」せよ

  Lecturer

  岡山大学 数学連携グループ・国立研究開発法人科学技術振興機構 (JST), 広がる数学 IX (第２８回 JST 数学キャラバン), From 23 Nov. 2018

  
• 軽量なプログラム検証のための要素技術

  Lecturer

  国立情報学研究所 オープンハウス2019：産官学連携セミナー 「形式手法・ソフトウェア工学の先端とさらに先：効率的テスト手法と機械学習・人工知能協働」, From 31 May 2019

  
• 安全性検証技術はビジネスになるか

  Lecturer

  第6回 Entrepreneur Candidate Club（ECC-iCAP） the place where science & entrepreneurship intersect ～科学のフロントランナーが語る未来世界～, From 17 May 2019

  
• そのプログラム、バグってないですか？：数学を使ってバグを見つけるための形式検証手法

  Lecturer

  2016年度情報処理学会関西支部定期講演会「IoT の周辺技術」, From 21 Dec. 2016

  
• そのプログラム、バグってないですか? ― 数学を使ってバグを見つける

  Lecturer

  JST 京都大学新技術説明会, From 24 May 2016

  
• プログラムの「正しさ」の話

  Lecturer

  膳所高校, From 05 Dec. 2015

  
• Validated Numerics Meets Reachability Analysis for CPS Design (NII Shonan Meeting 2015-14).

  Planner

  NII Shonan Meeting, From 2015