3月26日，应中国科学院外国特聘专家研究员、中法信息自动化与应用数学联合实验室LIAMA主任、数字所嵌入式软件系统研究中心Vania Joloboff教授邀请，法国国家科学研究中心（CNRS）、中法联合实验室LIAMA研究员Jean-Francois Monin教授到深圳先进技术研究院进行学术交流，并做了题为First Steps Towards the Certification of an ARM Simulator Using Compcert的学术讲座。

Monin教授简要介绍了嵌入式系统中系统级芯片（SoC）基于仿真器的快速开发方法，以及验证技术的应用场景。在Monin教授从事的研究中，使用法国国家信息及自动化研究院INRIA开发的Coq定理证明器对系统级芯片仿真器（SimSoC）进行验证。Monin教授以一条ARMv6处理器的ADC（Addition with Carry，带进位的加法）指令为例，讲述了在具体对基于Compcert-C的仿真器实施验证的过程和方法。随后，Monin教授还介绍了他及其团队在LIAMA于清华大学所做的研究项目以及所取得的成果。

本次讲座吸引了十多位研究人员和学生参加，现场气氛活跃。在讲述过程中，Monin教授详细回答了在场师生提出的问题。Joloboff教授对他本人及其团队开发的系统级芯片仿真器（SimSoC）相关细节进行补充说明。通过这次讲座，在场师生对形式化验证的概念及方法有了进一步清晰的认识。

Jean-Francois Monin是法国格勒诺布尔综合理工学院(Universite de Grenoble )/约瑟夫傅利叶(Joseph Fourier)大学教授、法国国家科学研究中心(CNRS)、中法信息自动化与应用数学联合实验室(LIAMA) 研究员。曾在法国电信研发部门工作，领导一个致力于形式化方法的研究团队，并将其成果成功地应用于工业框架下软件设备正确性的证明。2009年，担任法国国家科学研究中心研究员，并在中法信息自动化与应用数学联合实验室(LIAMA) 从事科研工作。他的研究领域主要包括Coq的理论型证明等，这些证明辅助实现了分布式算法的设计、安全问题的解决和嵌入式软件的实现等各项应用。