大规模软件基于抽象解释理论的时序性质验证及支持工具
批准号：
60703075
项目类别：
青年科学基金项目
资助金额：
18.0 万元
负责人：
李梦君
依托单位：
学科分类：
系统软件、数据库与工业软件
结题年份：
2010
批准年份：
2007
项目状态：
已结题
项目参与者：
李梦君、周会平、叶常春、马晓东、邢建英、陈石坤、余杰
项目摘要
结项摘要
项目成果
李梦君的其他基金
相似基金
相关文献
中文摘要
对大规模软件时序性质进行自动验证是一项十分有意义的研究工作。本课题以抽象解释理论中的抽象逼近方法作为基本理论工具，利用有效的数学计算工具软件，基于抽象-精化的迭代验证框架，以验证软件时序性质的高效抽象验证方法作为主要研究内容，需要解决的理论问题有：大规模软件面向验证性质的抽象迁移模型自动构造，不同抽象层次程序不变式的自动构造，包括安全性、活性性质在内的时序性质面向性质的一体化自动验证方法，基于虚假反例的抽象精化方法。在此基础上，基于函数式程序设计语言Objective-Caml,设计并实现支持大规模软件时序性质自动验证的工具原型系统。
英文摘要
期刊论文列表
专著列表
科研奖励列表
会议论文列表
专利列表
登录
查看更多内容
DOI：
--
发表时间：
--
期刊：
软件学报
影响因子：
--
作者：
[王杰生, 李梦君, 李舟军]
通讯作者：
李舟军
DOI：
--
发表时间：
--
期刊：
计算机研究与发展
影响因子：
--
作者：
[陈石坤, 李舟军]
通讯作者：
李舟军
DOI：
--
发表时间：
--
期刊：
计算机科学
影响因子：
--
作者：
[李舟军, 李梦君, 邢建英]
通讯作者：
邢建英
DOI：
--
发表时间：
--
期刊：
计算机工程与科学
影响因子：
--
作者：
[陈石坤, 李舟军]
通讯作者：
李舟军
DOI：
--
发表时间：
--
期刊：
软件学报，19(1),17-26,2008年1月。
影响因子：
--
作者：
[李梦君(*), 李舟军, 陈火旺]
通讯作者：
陈火旺
共 8 条
大规模软件验证若干关键技术研究及支持工具
-
批准号：61672525
-
项目类别：面上项目
-
资助金额：62.0万元
-
批准年份：2016
-
负责人：李梦君
-
依托单位：
含代数运算和时间特征的安全协议分析与验证
-
批准号：90604007
-
项目类别：重大研究计划
-
资助金额：28.0万元
-
批准年份：2006
-
负责人：李梦君
-
依托单位：
国内基金
海外基金