A blockchain is a distributed, replicated series of data records. It helps enforce the trust relationship between the parties who generate, and agree on, the on-chain data. Usually, programs called smart contracts can be written to define the business logics of the parties for producing new agreed-on data from existing data. Flaws in the design of blockchain protocols and programs (e.g., smart contracts) could lead to hijacked multi-party agreement on results favored by an attacker. In particular, if monetary data are affected, substantial economic loss could be resulted. In this talk, I introduce the basics of blockchains and smart contracts, and briefly outline the challenges in getting things right in their design and implementation. I then present some recent developments on the formal, deductive verification of smart contracts targeting the intermediate and high level smart contract languages. The concrete developments to be presented include a program logic for the formal verification of atomicity requirements for smart contracts at the source-level, and efforts in the formal verification of smart contracts expressed in the Ethereum intermediate language Yul.

李希萌，首都師范大學講師，碩士生導師。研究興趣為形式化驗證，目前主要關注區塊鏈程序和架構的形式化建模和定理證明。于2010年至2018年初在丹麥技術大學獲得碩士、博士學位，并先后在丹麥、德國開展博士后研究工作，主要研究方向為程序的信息流安全驗證。曾參加歐盟和德國科研項目2項，其中包括與空中客車公司的合作研發項目。現主持國家自然科學基金青年項目1項、北京市教委科技計劃一般項目1項。在形式化方法和信息安全領域重要期刊和國際會議發表論文十余篇，合著專著1部。

更多信息訪問李希萌的個人主頁：https://iec.cnu.edu.cn/szdw/sssds/js3/152042.htm