本课程为北京大学数学科学学院信息科学系课程，研本合上。
时间：每周二下午7-9节，15:10-18:00，2月27日开始上课。
地点：四教302。
主题：模型检查
教材：Christel Baier and Joost-Pieter Katoen. 《Principles of Model Checking》, the MIT Press, 2008.
课程介绍：
本课程将采取主讲教师讲授、特邀学者报告、学生报告结合的方式运行，学生于学期末课程结束之前需提交一篇与课程主题相关的研究论文并在课上报告论文相关工作，期末成绩会基于论文水平和报告表现决定。
主讲教师：孙猛
邀请报告人：待定
论文格式文件包从这里下载。
教学计划（暂定）：
| 2.27 | 第一讲：绪论 |
| 3.6 | 第二讲：并发系统建模 |
| 3.13 | 第三讲：线性时间性质（I） |
| 3.20 | 第四讲：线性时间性质（II），正则性质（I） |
| 3.27 | 第五讲：正则性质（II） |
| 4.3 | 第六讲：线性时态逻辑（I） |
| 4.10 | 第七讲：线性时态逻辑（II） |
| 4.17 | 第八讲：计算树逻辑（I） |
| 4.24 | 第九讲：计算树逻辑（II） |
| 5.1 | 五一放假停课一次。 |
| 5.8 | 第十讲：计算树逻辑（III），等价与抽象（I） |
| 5.15 | 第十一讲：等价与抽象（II） |
| 5.22 | 第十二讲：概率模型检查（I） |
| 5.29 | 第十三讲：概率模型检查（II） |
| 6.5 | 学生论文报告。 |
| 6.12 | 学生论文报告。 |
论文可选题目：
1. CTL model checking for Mediator models.
Reference: Li Yi and Sun Meng. Component-based Modeling in Mediator. In Proceedings of FACS 2017, pages 1-19, LNCS 10487, Springer, 2017.
2. Model checking timed Reo in UPPAAL.
Reference: Farhad Arbab, Christel Baier, Frank S. de Boer and Jan J. M. M. Rutten. Models and Temporal Logical Specifications for Timed Component Connectors. International Journal on Software and System Modeling. vol. 6(1), pages 59-82, 2007.
3. Model checking probabilistic connectors in PRISM / IscasMC.
Reference: Christel Baier. Probabilistic Models for Reo Connector Circuits. Journal of Universal Computer Science. vol. 11(10), pages 1718-1748, 2005.
4. Model checking smart contracts for blockchain.
Reference: Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv and Yoni Zohar. Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts. Proceedings of the ACM on Programming Languages, vol. 2, 2018.