4月17日-28日,在“南京航空航天大学境外专家短期来访”项目的支持下,法国图卢兹大学(Université de Toulouse) 安全关键软件领域专家Mamoun FILALI研究员、Jean-Paul BODEVEIX教授应邀来到计算机学院进行为期2周的学术交流。期间,黄志球副校长、陈兵院长会见了两位专家,并就未来学术合作研究、师生交流、高水平课程建设、国际项目申请、国际联合实验室等方面展开了深入的会谈。
4月26日下午,Mamoun FILALI研究员、Jean-Paul BODEVEIX教授与计算机学院软件工程团队老师进行了学术研讨,双方对各自的研究团队进行了介绍,并共同起草了南航-图卢兹大学校际合作协议,双方一致认为将在软件工程、形式化方法等领域展开深入切实的合作,包括共建形式化方法虚拟实验室(Virtual Lab on Formal Methods)、联合举办高可信软件春季国际讨论班和国际会议、申请中法自然基金、教师互访、中法航空航天计算机技术硕士培养项目等。此次会谈对中法两校开展实质性合作具有重要意义。
访问期间,两位专家于4月19日至26日在江宁校区计算机实验大楼102室,分别讲授《Introduction to the functional language: OCAML》、《Introduction to the formal development method B》两门专业核心课程,课程采用理论授课和上机实践结合的方式,共计15学时。计算机学院30余名师生参加了全部课程,上机实践与面对面讨论使得大家快速掌握学习内容,效果非常好。函数式程序设计语言OCAML具有安全编译、高效执行的特点,使其在代码生成器、模型转换、定理证明器Coq实现、多线程编程等方面有广泛使用。形式化方法Event-B,是一种基于集合论和模型求精(Refinement)的系统工程设计与验证方法,已经成功应用于诸如西门子地铁控制软件设计与开发。
4月27日,两位专家作了题为《Introduction to the proof assistant Coq》的学术报告,共计3学时。定理证明器Coq是基于类型系统的交互式定理证明的成功典范,已于2014年通过适航认证标准DO178B的工具鉴定,并被空客接受。Coq采用归纳构造演算对程序进行表达,对程序性质进行证明,并对证明序列本身的正确性进行验证,已经成为程序验证、编译器验证的重要工具。报告中,两位专家对我校师生提出的问题进行了详尽的解答,并围绕相关问题展开了深入讨论。
近年来,计算机学院不断加快国际化办学进程,通过访问、接洽国外计算机科学领域的顶级专家,了解国际科学发展前沿,学习办学经验,吸纳优秀人才和资源,为信息化与“三航”特色深度融合寻找新的支点。
背景链接:图卢兹大学(Université de Toulouse),建校于1229年,是一所位于法国南部-比利牛斯大区的世界著名大学,为欧洲经济学和法国工科的最高学府,同时也是法国政府重点发展的8所大学之一,法国高等教育“卓越计划”主要成员之一。图卢兹大学以航空航天工程的欧洲最高学府闻名于世,是空中客车(航空)和EADS Astrium(航天)等高科技公司的最主要支持力量。目前,图卢兹大学由4所综合性大学、7所工程师学院、1所建筑学院、1所商学院和1所政治学院组成,并拥有5所国际科研机构,200所研究实验室、145家科研单位。