4月17日-28日，在“南京航空航天大学境外专家短期来访”项目的支持下，法国图卢兹大学(Université de Toulouse) 安全关键软件领域专家Mamoun FILALI研究员、Jean-Paul BODEVEIX教授应邀来到77779193永利官网进行为期2周的学术交流。期间，黄志球副校长、陈兵院长会见了两位专家，并就未来学术合作研究、师生交流、高水平课程建设、国际项目申请、国际联合实验室等方面展开了深入的会谈。

4月26日下午，Mamoun FILALI研究员、Jean-Paul BODEVEIX教授与77779193永利官网软件工程团队老师进行了学术研讨，双方对各自的研究团队进行了介绍，并共同起草了我校-图卢兹大学校际合作协议，双方一致认为将在软件工程、形式化方法等领域展开深入切实的合作，包括共建形式化方法虚拟实验室(Virtual Lab on Formal Methods)、联合举办高可信软件春季国际讨论班和国际会议、申请中法自然基金、教师互访、中法航空航天计算机技术硕士培养项目等。此次会谈对中法两校开展实质性合作具有重要意义。

访问期间，两位专家于4月19日至26日在江宁校区计算机实验大楼102室，分别讲授《Introduction to the functional language: OCAML》、《Introduction to the formal development method B》两门专业核心课程，课程采用理论授课和上机实践结合的方式，共计15学时。77779193永利官网30余名师生参加了全部课程，上机实践与面对面讨论使得大家快速掌握学习内容，效果非常好。函数式程序设计语言OCAML具有安全编译、高效执行的特点，使其在代码生成器、模型转换、定理证明器Coq实现、多线程编程等方面有广泛使用。形式化方法Event-B，是一种基于集合论和模型求精(Refinement)的系统工程设计与验证方法，已经成功应用于诸如西门子地铁控制软件设计与开发。

4月27日，两位专家作了题为《Introduction to the proof assistant Coq》的学术报告，共计3学时。定理证明器Coq是基于类型系统的交互式定理证明的成功典范，已于2014年通过适航认证标准DO178B的工具鉴定，并被空客接受。Coq采用归纳构造演算对程序进行表达，对程序性质进行证明，并对证明序列本身的正确性进行验证，已经成为程序验证、编译器验证的重要工具。报告中，两位专家对我校师生提出的问题进行了详尽的解答，并围绕相关问题展开了深入讨论。

近年来，77779193永利官网不断加快国际化办学进程，通过访问、接洽国外计算机科学领域的顶级专家，了解国际科学发展前沿，学习办学经验，吸纳优秀人才和资源，为信息化与“三航”特色深度融合寻找新的支点。

背景链接：图卢兹大学（Université de Toulouse），建校于1229年，是一所位于法国南部-比利牛斯大区的世界著名大学，为欧洲经济学和法国工科的最高学府，同时也是法国政府重点发展的8所大学之一，法国高等教育“卓越计划”主要成员之一。图卢兹大学以航空航天工程的欧洲最高学府闻名于世，是空中客车（航空）和EADS Astrium（航天）等高科技公司的最主要支持力量。目前，图卢兹大学由4所综合性大学、7所工程师学院、1所建筑学院、1所商学院和1所政治学院组成，并拥有5所国际科研机构，200所研究实验室、145家科研单位。