刘嘉祥，博士，助理教授，硕士生导师，深圳市海外高层次C类人才。2010年毕业于清华大学软件学院，获工学学士学位；2017年6月毕业于清华大学计算机科学与技术系，获工学博士学位，并于同年10月获得法国巴黎萨克雷大学的计算机博士学位。2017年11月加入开yun体育官网入口登录苹果，任博士后研究员；2020年5月获聘为开yun体育官网入口登录苹果助理教授。目前主要从事形式化验证（Formal Verification）方面的研究，包括软件验证（Software Verification）、神经网络验证（Neural Network Verification）、系统建模与验证（System Modeling and Verification）和重写理论（Rewriting Theory）等。相关成果发表在CAV、ASE、CCS、Theoretical Computer Science (TCS)、IEEE Trans. on Industrial Electronics (TIE) 等国际知名学术会议/期刊。目前主持1项广东省自然科学基金面上项目、1项深圳市稳定支持计划项目，曾主持及参与多项国家自然科学基金项目。

=== 欢迎对我研究方向感兴趣的同学与我联系 ===

研究方向简介（我的论文发表列表可以参考[这里]）

形式化验证：在系统开发的过程中，无论硬件系统还是软件系统，系统质量都是开发人员和用户最关心的问题。正确性/可靠性作为最主要的系统质量衡量标准，在一些重要的应用场景（如飞机控制、自动驾驶、区块链等）中甚至直接影响人们的生命和财产安全。传统的系统质量保障方法主要有测试技术与仿真技术，但它们却无法100%保证系统的正确性，因为测试人员无法对系统的所有可能性进行测试或仿真。形式化验证技术可以利用数学方法去证明系统中不存在bug，可以100%保证系统的正确性，早已被工业界应用于硬件系统的开发过程中，而如今也越来越多地受到软件开发人员的重视，如华为的鸿蒙OS 和百度的MesaTEE 安全计算平台，都应用了形式化验证技术。

软件验证：软件验证技术是利用自动化的形式化技术，如抽象（abstraction）、模型检验（model checking）、约束求解（constraint solving）等，直接对软件的源代码进行正确性检查。我们目前已开发出一套方法和工具，并对许多工业界使用的真实代码进行了应用。

神经网络验证：神经网络作为人工智能的主要技术，近年来得到了广泛的应用，甚至开始被应用到许多安全攸关的场景，如自动驾驶。然而科学界目前仍无法很好地解释神经网络的工作原理，其正确性/可靠性也无法得到保障，现实中特斯拉的自动驾驶系统已导致多起事故。我们希望利用形式化验证技术对神经网络的正确性进行检查，为神经网络应用的安全性提供保障。

系统建模与验证：系统建模技术主要针对无法自动分析的系统，如软硬件协同系统、网络协议、分布式系统等，进行手工的分析、理解和建模，并利用形式化验证工具对得到的抽象模型进行正确性验证。

重写理论：重写系统（rewriting systems）是一种可用于描述非确定性（non-deterministic）计算（如并行计算）的抽象模型。一个重写系统如果满足合流性（confluence），表示该系统所描述的非确定性计算将具有确定性的计算结果。我们关注对重写系统合流性的检查方法。