2011年暑期，为期9天的第三届亚太地区形式化方法暑期学校在中国科学技术大学苏州研究院正式开学。多位著名的国际学者应邀为本次暑期学校授课，来自国内外21所高校与科研院所的81名学员踊跃报名并积极参加了暑期学校。
图：来自法国波尔多第一大学Pierre Casteran教授正在授课
亚太地区形式化方法暑期学校由中法信息、自动化与应用数学联合实验室（LIAMA）于2009年发起。形式化方法是信息学科的重要研究领域，是美国麻省理工《科技创业》（Technology Review）杂志今年评选出的2011年度十大新兴技术之一“防崩溃代码”（Crash-Proof Code）所采用的主要技术手段。本次暑期学校由法国国家信息与自动化研究院的Yves Bertot研究员和法国波尔多第一大学的Pierre Casteran教授系统进行讲授，并介绍与之相关的定理证明辅助工具Coq；由法国雷恩第一大学的Sandrine Blazy教授介绍处于国际前沿的CompCert编译器验证技术；由国际知名专家——美国微软研究院Chris Hawblitzel博士、耶鲁大学邵中教授和中科大苏州研究院冯新宇教授——进行防崩溃代码的研究专题介绍。参加暑期学校的学员有来自中科院、清华大学、北京大学、南京大学、华东师范大学、浙江大学、国防科学技术大学等工作在国内高校一线的研究生与教师，也有来自法国约瑟夫•傅里叶大学、美国普林斯顿大学和香港中文大学的学生；学员的专业涵盖了计算机科学、计算机工程、软件工程、数学及物理等各个专业。本次暑期学校还作为中科大本科生“计算机软件与理论前沿”暑期课程，28名来自中科大计算机、数学和少年班等学院的本科生选修了本课程。
图： 来自法国INRIA的Yves Bertot研究员正在授课
为了使得学员能够更好地理解所讲授的知识，本次暑期学校采取了理论联系实际的课程安排。上午的课程为理论教学，下午的课程为上机实验。课上课下专家们与学员开展了大量的交流与讨论。中科大-耶鲁高可信软件联合研究中心派出10多名师生承担上机实验的助教工作，帮助学员熟悉实验环境，解答疑难问题。学员们一致认为获益匪浅。在课程的最后一天，来自国内外5所大学的研究团队的代表还展示了在形式化方法领域取得的最新的研究成果，使学员了解到所学内容在前沿研究领域的应用与最新进展，并进一步加深了学员之间的交流。广大学员对本次暑期学校的授课效果与组织安排表示非常满意。
图：学员们正在上机实践
本次暑期学校的举办获得了独墅湖高教区和中科大苏州研究院的大力支持，并获得了来自中法信息、自动化与应用数学联合实验室和清华大学软件学院的大量帮助。参加暑期学校的同学得以与国内外各高校的研究生与教师一起生活学习，并进行深入的交流，对于我院在该领域的研究生教育和高水平研究人才培养将产生重要的推动作用。暑期学校为国内外学者交流形式化方法前沿进展搭建了一个良好的平台，进一步加强了我院与一流学者的学术交流，对于推动我院学科合作、交流与发展，提高了研究院在本领域的国际学术声誉有着重要意义。
图： 学员们在认真听讲
图： 专家和学员合影
