郑剑锋清华大学 清华大学第五届亚太地区形式化方法暑期学校(2013)招生通知
2013.8.5-10,清华大学,北京 第五届亚太地区形式化方法暑期学校(5th Asian-Pacific Summer School on Formal Methods,APSSFM 2013)将于2013年8月5-10日在清华大学举办,欢迎计算机、软件、数学、物理及相关专业同学和学者报名。
亚太地区形式化方法暑期学校是由清华大学,中法信息、自动化与应用数学联合实验室(LIAMA)共同发起,以培养亚太地区计算机软件与理论研究与应用人才为目标的专题教学和学术交流活动,每年邀请国际知名学者讲授交互式定理证明工具Coq的原理、编程方法、其在软件正确性研究中的应用、最新研究进展等。
自2009年以来,先后由清华大学(2009,2010),中国科技大学(2011),华东师范大学(2012)主办,已经有来自国内外数十所高校和研究所的近300名研究生、学者参加了学习。
Coq是一个开源编程环境,它支持函数式编程,并提供了基于类型论的高阶逻辑推理框架,同时能保证所开发的证明是正确的。
它可用于程序建模和程序性质分析,它所支持的交互式定理证明技术是当前软件正确性和可信性研究的主流方法之一。Coq以表达能力强,应用范围广和开放性著称,欧美不少学者从事Coq相关基础研究,或将其作为形式化方法研究工具或软件基础教学工具。
它在一些重要领域如数学定理证明(如四色定理、Feit-Thompson定理的首个形式化证明),以及工业级安全攸关产品验证(如智能卡内核,C语言编译器,操作系统)等已获得成功应用。
今年特色 今年将首次以优秀本科生为主要对象举办暑期学校,课程内容和形式针对本科生知识背景做了优化。为鼓励国内本科拔尖人才探索软件专业学科前沿,今年的暑期学校除免收注册和住宿费外,将由主讲教师提名优秀学员予以奖励,对符合条件的中国大陆地区本科学员提供往返差旅资助,对表现优异的学员在申请推免清华大学硕、博研究生考察时给予优先考虑。
暑校也为研究生和同行学者预留了名额,同样欢迎报名参加。 教学安排 今年的暑期学校将讲授Coq的基本编程技术和基于Coq的程序正确性证明方法。主题包括递归程序设计,表和整数处理,归纳证明,自定义数据类型,基于模式匹配和分类的推理等。
课程将用英语讲授,采用半天授课、半天上机实习的方法进行,上机实习会有授课教师和助教现场辅导,课程最后会有一个挑战性测试。已确定来校学习的学员可先行下载安装Coq软件。
课程将用英语讲授。上课地点位于清华大学校内。 报名和录取 1、面向计算机、软件、数学、物理及相关专业的本科生、研究生和学者招生。
2、尤其欢迎有较好数学素养、富有探索精神的优秀本科生报名参加。 3、对报名者的先修课程没有要求,只要求掌握至少一种程序设计语言编程技术。
4、报名需下载并填写报名表邮件寄回,在校生需提供成绩单(详情见暑期学校主页)。 5、根据报名信息择优录取,招生总人数不超过30人。
6、录取通知将通过邮件发送,并在主页上公布(姓名拼音,学校名),未录取不另发通知。 7、入学需自备笔记本电脑。
费用和资助 1、免收注册费(10年、11年、12年的在校生注册费分别为100、400和600元)。
2、清华大学提供免费食宿(校内集体宿舍和校内食堂)。 3、学校和家庭所在地均不在北京的本科三年级同学,可申请旅费资助。获资助资格的同学如在暑校结束时达到结业标准,可报销往返旅费。
认证和奖励 1、暑校结束时,考勤和课程练习达到结业标准的学员,发结业证书。 2、由授课教师推荐课程学习成绩最优秀的1-3名学员,结业时为其颁发"杰出表现学员"证书或予以奖励。
