我单位下列项目参与申报2016年度高等学校科学研究优秀成果奖（科学技术），现将项目信息予以公示，公示期自2015年5月9日至 2015年5月13日。公示期内如有异议，可向北京大学科学研究部反映，异议人需用真实姓名，并提供手机号码、电子邮件等联系方式；异议单位书面材料需加盖单位公章。
联系人： 王纬超
联系电话： 010-62751439
电子邮箱： wwc@pku.edu.cn
北京大学科学研究部
2016.5.9
附:公示内容
推荐奖种：国家自然科学奖（直报）
项目名称：程序验证的基础理论研究
推荐单位：西安电子科技大学
项目简介:如何保障软件系统的正确性和可靠性是计算机软件领域面临的重要挑战。图灵奖获得者Clarke等人提出的模型检测方法是迄今为止最成功的自动化程序验证方法。程序性质的描述、模型的提取以及检测算法是模型检测的三要素。但是在这三方面均存在一些亟待解决的问题：（1）性质描述语言表达能力不足；（2）系统模型难以提取；（3）状态空间爆炸。针对这些问题，本项目提出了一套基于时序逻辑的程序验证理论：用命题投影时序逻辑（PPTL）描述系统的性质，用投影时序逻辑统一验证技术使得系统和模型的描述在同一逻辑体系，用高效的抽象模型检测方法缩减状态空间，从三个方面克服程序验证的三个问题。具体创新点如下：
1. 建立了投影时序逻辑PTL的模型理论，严格定义了PTL和PPTL的语法和语义，提出并证明了该逻辑的182个定理和536个逻辑规则；建立了PTL和PPTL的公理系统，并证明了其合理性和完备性；解决了PPTL和基于区间的命题时序逻辑PITL的判定难题；证明了基于区间的时序逻辑的非初等复杂性及PPTL的完全正则表达能力；提出了多核并发程序形式化模型，即柱面计算模型，给出了其语法、语义、逻辑规则和操作语义，提高了性质描述语言的表达能力。
2. 提出了以投影时序逻辑PTL可执行子集为基础的集建模、仿真和验证为一体的并行程序设计语言MSVL，给出了MSVL的最小模型；解决了时序逻辑面向实际程序设计中的框架难题；建立了基于MSVL的集建模、仿真和验证为一体的统一验证理论，使得程序模型和性质的描述在同一逻辑体系，避免了程序验证中模型提取的困难。
3. 提出了多项式抽象模型精化算法，避免了原精化方法中的指数爆炸；提出了线性虚假路径检测算法，克服了原虚假反例路径检测中的多项式时间复杂度；提出了高效的网络系统模型状态空间缩减方法和分布式网络的验证算法，有效缩减网络软件系统模型检测中的状态空间，提高了验证效率。
主要完成人情况表：
序号
完成人
所在单位
创新性贡献
1
段振华
西安电子科技大学
投影时序逻辑的模型理论和公理系统，MSVL语言及其语义，混合系统的验证，抽象模型检测
2
田 聪
西安电子科技大学
命题投影时序逻辑的可判定性和抽象模型检测理论和方法
3
堵宏伟
哈工大深圳研究生院
针对网络系统的状态空间缩减理论
4
崔 斌
北京大学
针对分布式网络的验证理论和方法
5
张 南
西安电子科技大学
投影时序逻辑的公理系统及多核并行计算模型
代表性论文专著目录：
1. Zhenhua Duan, Temporal Logic and Temporal Logic Programming, Science Press, 2005年
2. Zhenhua Duan, Modeling and Analysis of Hybrid Systems, Science Press, 2004年
3. Zhenhua Duan, Cong Tian, Li Zhang, A Decision Procedure for Propositional Projection Temporal Logic With Infinite Models, Acta Informatica, 2008年45卷43-78页
4. Zhenhua Duan, Xiaoxiao Yang, Maciej Koutny, Framed Temporal Logic Programming, Science of Computer Programming, 2008年70卷31-61页
5. Nan Zhang, Zhenhua Duan, Cong Tian, A cylinder computation model for many-core parallel computing, Theoretical Computer Science, 2013年497卷68-83页
6. Weili Wu, Hongwei Du, Xiaohua Jia, Yingshu Li, Scott C.-H. Huang, Minimum Connected Dominating Sets and Maximal Independent Sets in Unit Disk Graphs, Theoretical Computer Science, 2006年352卷1-7页
7. Hongwei Du, Weili Wu, Qiang Ye, Deying Li, Wonjun Lee, Xuepeng Xu, CDS-Based Virtual Backbone Construction with Guaranteed Routing Cost in Wireless Sensor Networks. IEEE Trans. Parallel Distrib. Syst. 2013年 24卷: 652-661页.
8. Bin Cui, Hua Lu, Quanqing Xu, Lijiang Chen, Yafei Dai, Yongluan Zhou, Parallel Distributed Processing of Constrained Skyline Queries by Filtering, ICDE 2008, 546-555页
