欢迎您！东篱公司
退出
-
申报数据库
-
立项数据库
-
成果数据库
-
项目获奖数据库
位置：立项数据库 > 立项详情页
中文摘要：
面向性质的可信软件建模与时序性质验证及支持工具具有重要的研究价值。本课题以抽象解释理论中的逼近计算作为抽象复杂计算的理论工具，结合软件测试和软件验证方法中的路径条件、偏序消减、符号化执行、约束求解、惰性计算等多种技术，以验证可信软件的时序性质作为主要研究内容，需要解决的理论问题有可信软件面向性质的高精度程序切片方法，可信软件面向验证性质的抽象迁移模型构造，基于反例制导的抽象精化迭代验证框架的可信软件时序性质的有效验证方法。在此基础上，基于函数式程序设计语言Objective-Caml,设计并实现支持可信软件时序性质自动验证的工具原型系统。
结论摘要：
英文主题词program slice; abstract transition model construction; formal verification; temporal property;counterexample-guided abstract refinemnet iterative veri
成果综合统计
期刊论文
会议论文
专利
获奖
著作
期刊论文
相关项目
李舟军的项目
