形式化方法
课程编码：081202M05001H
英文名称：Formal Methods
课时：40
学分：2.00
课程属性：专业普及课
主讲教师：张文辉
教学目的要求
教学目的和要求：
本课程为计算机软件与理论学科研究生的专业普及课。本课程讲授和讨论形式化方法前沿研究领域的主要思想和关键技术。主要内容有软件系统抽象模型、程序与时序逻辑、软件系统模型的分析与验证等。
通过本课程的学习，希望学生能了解形式化方法的前沿研究领域，了解软件系统分析与验证方法方面的最新研究成果，掌握基本思想和关键技术，培养学生形式化方法方面的研究能力。
预修课程
数理逻辑与程序理论、形式语言与自动机理论
大纲内容
第一章 形式化方法
第1节 绪论 3学时
第2节 程序与软件系统模型 15学时
第3节 时序逻辑 9学时
第4节 基于演绎推理的验证方法 9学时
第5节 基于模型检测的验证方法 2学时
第6节 课程总结 1学时
参考书
1、
The Foundation of Program Verification
J. Loeckx and K. Sieber
1984.0
Wiley & Sons Ltd
课程教师信息
张文辉，
中国科学院软件研究所计算机科学国家重点实验室研究员。
1963年生。
1988年获挪威奥斯陆大学博士学位。
2000年入选中国科学院 “引进国外杰出人才计划”。
获2008年度中国科学院朱李月华优秀教师奖。
主要研究方向包括形式模型、数理逻辑与程序逻辑、推理与模型检测、计算机软件正确性的理论与方法。