2019年CCF龙星计划—《逻辑与形式化方法》课程成功举办

2019年8月7-9日，由中国计算机协会主办、上海科技大学与复旦大学联合承办、CCF形式化方法专委会提供支持的2019年CCF龙星计划《逻辑与形式化方法》课程在上海科技大学创管学院报告厅成功举办。本次课程由美国西密歇根大学杨子江教授讲授，面向高等院校和产业界人士招生，吸引了来自清华大学、香港中文大学、捷克理工大学和上海华为技术有限公司等国内外85个单位的近100名高校学生、专家学者、技术总监等报名参加。本次《逻辑与形式化方法》课程是上海科技大学首次举办龙星计划课程，课程的举办填补了信息学院在计算机理论课程方面的空白，促进了模型检测技术原理和应用实践的产学研融合，也增进了外单位学员对上海科技大学和信息学院的了解。

杨子江教授（一排正中）、宋富教授（一排右二）与课程学员合影留念

上海科技大学宋富教授进行课程介绍

近年来，随着信息技术的广泛应用，特别是信息技术与物理世界和人类社会的高度融合，整个社会的信息化程度不断提高，人们对计算机系统的可靠性与安全性提出了更高的要求。计算机系统的错误及安全隐患影响到生命财产安全。形式化方法是保证计算机系统正确性和安全性的一种重要方法，其采用数学逻辑证明的手段对计算机系统进行建模、规约、分析、推理和验证。在此背景下，中国计算机学会特邀杨子江教授参与CCF龙星计划，讲授计划逻辑与形式化方法课程。

杨子江教授授课中

杨教授课后与学员交流

在为期三天的课程中，杨教授授课过程将电子课件与板书相结合，整个课程涵盖了时序逻辑、基于BDD的模型验证、SAT、SMT、偏序约减等内容，讲解深入浅出，课时之间连贯性强，与学员交流互动频繁。课程视频已被CCF数字图书馆收录。课程结束后，杨教授也与参与课程的学员及专家学者就相关领域研究展开了深入的交流。通过技术理论学习和应用实践相结合，学员们加深了对形式化方法、模型检测基本知识的理解，初步掌握了形式化方法在程序、实时系统和信息物理系统中自动化验证的应用方法。学员们普遍对本次龙星课程的授课质量与服务保障给予高度评价。来自上海科技大学的高鹏飞同学表示，本次课程系统地梳理了逻辑与形式化方法的相关知识，使自己对该领域的起源、现状与未来发展方向有了整体的认识，加深了自己对模型检查的理解；同时也促进了自己与其他高校的相关研究人员交流沟通，收获颇多，受益匪浅。

延伸阅读：

杨子江教授，深信科创创始人，分别从中国科学技术大学，美国赖斯大学(Rice University)及宾夕法尼亚大学(University of Pennsylvania)获得学士，硕士及博士学位。曾供职于NEC美国研究院及贝尔实验室。获得2018 ACM SIGSOFT Distinguished Paper Award, 2018 Google Engagement Award, 2010 PADTAD best paper award, 2008 ACM TODAES best paper award and the 2008 CEAS outstanding new researcher award等奖项。担任中美科学基金评委，美国能源部小企业基金评委，2019年IEEE软件测试验证会议主席等职。

CCF龙星计划是由中国计算机学会发起的公益性计划。该计划通过组织在美国学术界拥有较高学术声望的华人教授，回国系统地讲授一门美国研究生课程（每门课程15~30课时）。以促进我国相关领域的发展。课程面向全国相关领域的教师、学生以及企业界人士，学员免费参与相关学习。2019年度的龙星计划《逻辑与形式化方法》课程面向计算机、软件工程、可信计算等专业的相关人员，内容侧重于模型检测技术原理和应用实践。