国家自然科学基金(90718039)

作品数：4被引量：15H指数：3
导出分析报告
相关作者：顾明苏开乐骆翔宇更多>>
相关机构：清华大学桂林电子科技大学北京大学更多>>
相关期刊：《北京大学学报（自然科学版）》《Journal of Zhejiang University-Science A(Applied Physics & Engineering)》《Science China(Information Sciences)》《计算机学报》更多>>
相关主题：MODEL_CHECKINGPLC可编程序控制器定理证明器定理证明更多>>
相关领域：自动化与计算机技术电子电信理学更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-4
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
Competent predicate abstraction in model checking被引量：4
《Science China(Information Sciences)》2011年第2期258-267,共10页LI Li SONG XiaoYu GU Ming LUO XiangYu 
supported by the National Basic Research Program of China (Grant No. 2004CB719406);the National Natural Science Foundation of China (Grant Nos. 60635020, 90718039, 60763004)
The paper presents a new approach to computing the abstract state and a maximum weight heuristic method for finding the shortest counter-example in verification of imperative programs. The strategy is incorporated in ...
关键词：PROGRAM model checking predicate abstraction weight heuristic 
一种求解认知难题的模型检测方法被引量：5
《计算机学报》2010年第3期406-414,共9页骆翔宇 苏开乐 顾明 
国家自然科学基金重点项目(90718039);国家"九七三"重点基础研究发展规划项目基金(2010CB328103);国家杰出青年科学基金(60725207);国家自然科学基金(60763004);广西青年科学基金(桂科青0728090);中国博士后科学基金(20090450389)资助
用公告逻辑建模并求解和与积认知难题.提出一种动态认知模型,将环境认知模型与公告导致的认知模型线性组合,从而在时态认知逻辑模型检测技术中扩展支持公告逻辑的建模与验证.该模型检测方法不仅可以用于搜索认知难题的所有解,而且可以...
关键词：模型检测 OBDD 公告逻辑 时态认知逻辑 和与积难题 
COQ定理证明器辅助PLC程序验证和分析被引量：6
《北京大学学报（自然科学版）》2010年第1期30-34,共5页陈钢 宋晓宇 顾明 
国家自然科学基金资助项目(90718039)
使用定理证明器COQ验证和分析PLC抢答器程序的一些性质,证明了原程序的所有可能状态中只有半数是可达状态,揭示了系统在可达状态之间的转移关系。基于这些性质,引入了逻辑自动机的概念作为对PLC程序行为完整抽象的描述。此外,在证明过程...
关键词：可编程序控制器 PLC 嵌入式系统 COQ 定理证明 
Equality detection for linear arithmetic constraints
《Journal of Zhejiang University-Science A(Applied Physics & Engineering)》2009年第12期1784-1789,共6页Li LI Kai-duo HE Ming GU Xiao-yu SONG 
Project supported by the National Natural Science Foundation of China (Nos 60635020 and 90718039);the National Basic Research Program (973) of China (No 2004CB719406)
Satisfiability modulo theories (SMT) play a key role in verification applications. A crucial SMT problem is to combine separate theory solvers for the union of theories. In previous work, the simplex method is used to...
关键词：Model checking Satisfiability modulo theories （SMT） Linear arithmetic 
全选清除导出
共1页<1>
检索报告 对象比较 聚类工具 使用帮助 返回顶部