高可信软件技术

课程编码：280216085405P3001 英文名称：Technologies for Trustworthy Software 课时：40 学分：2.00 课程属性：专业课 主讲教师：张健等

本课程是为电子信息专业研究生开设的专业普及课，其目的是使学生掌握高可信软件质量保障的基本原理和方法。通过课程教学，使学生掌握常用的软件规约与建模方法、测试与分析方法以及形式验证技术，并能够使用相关软件测试、分析与验证工具进行实践。

程序设计语言、离散数学、软件工程

第一章 绪论
第1节 高可信软件概述 3学时 张健
第二章 软件测试与分析
第1节 黑盒测试 3学时 张健
第2节 白盒测试 3学时 张健
第3节 符号执行 3学时 张健
第4节 程序分析 3学时 张健
第三章 新型软件测试与分析
第1节 并发测试 6学时 吴鹏
第2节 黑盒AI测试 3学时 吴鹏
第3节 白盒AI测试 3学时 吴鹏
第四章 软件形式建模与验证
第1节 形式建模 4学时 朱雪阳
第2节 形式验证 3学时 朱雪阳
第3节 模型检测 6学时 朱雪阳

张健，中国科学院软件研究所研究员。主要研究兴趣包括：自动推理、约束求解、软件测试与分析。曾先后获得中创软件人才奖、国家杰出青年科学基金、国务院政府特殊津贴，指导的多名研究生获得了中国科学院院长奖、中国计算机学会优秀博士论文提名奖等荣誉。目前担任《计算机学报》，J. of Computer Sci. and Tech.，Frontiers of CS，IEEE Trans. on Reliability，《计算机科学与探索》编委。
朱雪阳，中国科学院软件研究所副研究员。主要研究方向为：嵌入式系统设计、形式化方法、智能合约分析与验证等。
吴鹏，中国科学院软件研究所副研究员、硕士生导师。主要研究兴趣包括：并发理论、并发程序的形式化验证和测试、机器学习等。曾主持、参与多项国家自然科学基金项目、国家重点研发计划项目；在相关领域重要国际会议ATVA、ICECCS和期刊IEEE Transactions on Software Engineering、Information and Software Technology等发表多篇学术论文；担任中国科学院大学《多处理器系统编程》、《软件测试与安全分析》和《并发数据结构与多核编程》等课程的主讲教师。