第10回ステアラボソフトウェア技術セミナー『スマートコントラクトアプリケーションの形式検証』のご案内

[安部達也]

皆様、

千葉工大の安部達也です。今月末に東北大の西田雄気さんにスマートコントラク
トアプリケーションの形式検証に関する講演をしていただけることになりました。

ぜひこの機会をご利用ください。

日時：2026年6月30日（火）13:00〜14:00
場所：オンライン
参加費：無料
参加方法：https://stair-st.connpass.com/

講師：西田雄気 様
演題：スマートコントラクトアプリケーションの形式検証
概要：
「ブロックチェーン」という言葉を聞いた時に真っ先に思い浮かぶのは日々のニュースなどで目にする暗号通貨でしょうか？イーサリアム以降，多くのブロックチェーンプラットフォームでは通貨の送受金といった組み込みの処理に加えてユーザーの書いた自由なプログラムをチェーン上に登録し実行するという機能が備わっています．こうしたプログラムのことを「スマートコントラクト」と呼びますが，取り扱うデータの資産価値の高さ・プログラムの公開性・顕在的な管理者の不在といった特有の事情から事前に検証することが重要なものとなっています．
本講演ではブロックチェーンシステムの軽い紹介から始め，ソフトウェア検証という視点から見た特徴的なシステムの側面を紹介したのち，ICBC2024で発表された"iCon:
Automated Verification of Inter-Transaction Properties in Tezos Smart
Contracts with Unknowns"を元にスマートコントラクトアプリケーションに対する形式検証アプローチの一つを紹介します．当検証で扱う性質はいわゆる安全性であり，より具体的には明示的に与えた不変条件の検証を行いますが，技術的な困難の一つとして検証者のあずかり知らぬ外部のスマートコントラクトとのインタラクションをどう扱うかという点があります．講演の後半ではこうした部分について関連研究との比較も交えつつ検証手法の形式化の紹介を行います．


問合せ先：安部達也 <abe.t...@chibatech.ac.jp>