报告题目：Is your code correct?
报告人：Arm，熊沙乐研究工程师
报告时间：2023年5月25日（周四）下午16:00
报告地点：犀浦校区3号教学楼31541
主持人：李天瑞教授
报告摘要：
The talk provides an overview of recent public work on verifying the specification and prototype of the Realm Management Monitor (RMM). The RMM is an essential firmware component of Arm Confidential Computing Architecture (Arm CCA), which is a recently announced Confidential Computing technology incorporated in the Armv9-A architecture. The second part of the talk introduces notable research contributions from various scholars in the field of formal verification over the past 20 years.
报告人介绍：
Shale Xiong is currently a research engineering at Arm, focusing on formal verification and information security. His work involves examining specifications, protocol designs, software implementations, and prototyping verification and validation strategies to enhance their quality and security. He received his PhD degree in Computer Science from Verified Trustworthy Software Specification Group at the Department of Computing, Imperial College, in 2019, and received his Bachelor’s degree in Software Engineering from Southwest Jiaotong University, China, in 2014.