形式化方法
课程编码：180086081202M3001H
英文名称：Formal Methods
课时：40
学分：2.00
课程属性：专业课
主讲教师：朱雪阳等
教学目的要求
本课程讲授和讨论形式化方法研究领域的基础理论和关键技术。主要内容有软件系统抽象模型、时序逻辑、软件系统抽象模型的时序逻辑性质的分析与验证方法等。通过本课程的学习，学生有望了解形式化方法的基本思想和软件系统分析与验证方法方面的研究成果，掌握基础理论和关键技术，培养学生形式化方法方面的研究能力。
预修课程
数理逻辑与程序理论、形式语言与自动机理论
大纲内容
第一章 形式化方法
第1节 绪论 3学时 朱雪阳
第2节 程序与软件系统模型（1） 3学时 施晓牧
第3节 基于演绎推理的验证方法 9学时 施晓牧
第4节 程序与软件系统模型（2） 12学时 朱雪阳
第5节 时序逻辑 9学时 朱雪阳
第6节 基于模型检测的验证方法 2学时 朱雪阳
第7节 课程总结 1学时 朱雪阳
参考书
1、
The Foundation of Program Verification
J. Loeckx and K. Sieber
1984
Wiley & Sons Ltd
2、
Model Checking
E. M. Clarke, O. Grumberg and D. Peled
1999
The MIT Press
3、
Software Reliability Methods
D. A. Peled
2001
Springer-Verlag
4、
Principles of Model Checking
C. Baier and J.-P. Katoen
2008
MIT Press
5、
Verification of Sequential and Concurrent Programs
K. R. Apt, F. S. de Boer and E.-R. Olderog
2009
Springer-Verlag
课程教师信息
朱雪阳，中国科学院软件研究所副研究员、硕士生导师。主要研究方向为：嵌入式系统设计、形式化方法、智能合约分析与验证等。曾主持、参与多项国家自然科学基金项目、国家重点研发计划项目；在相关领域重要国际会议和期刊I发表多篇学术论文；担任中国科学院大学《高可信软件工程》等课程的主讲教师。个人学术主页：http://lcs.ios.ac.cn/~zxy/
施晓牧，中国科学院软件研究所高级工程师、硕士生导师。主要研究方向为：使用定理证明器对计算机软硬件基础设施的正确性与安全性进行形式验证，包括编译器、密码程序、SMT求解器等。主持国家自然科学基金青年基金、广东省自然科学基金面上项目、深圳市自然科学基金面上项目各一项；论文发表于CAV、CCS、ASE等国际会议。