谓词抽象

作品数：24被引量：47H指数：4
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：屈婉霞魏燕侠郭阳李暾任强更多>>
相关机构：清华大学国防科学技术大学苏州大学武汉大学更多>>
相关期刊：《计算机应用》《世界哲学》《计算机学报》《天津理工大学学报》更多>>
相关基金：国家自然科学基金国家社会科学基金江苏省高校自然科学研究项目江苏省自然科学基金更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
关于C语言程序安全验证中K-归纳法的改进
《天津理工大学学报》2024年第5期108-113,共6页侯春燕 白静媛 陈晨 
天津市新一代人工智能科技重大专项(19ZXZNGX00080);NFSC-通用技术基础研究联合基金(U1936105)。
过去几年中,程序验证技术在学术界和工业界获得了越来越多的青睐。K-归纳法是一种著名的软件模型检查技术,其结合了有界模型检查和归纳法来验证程序安全。许多软件验证工具已经将其实现。该方法在有限的时间内展开循环,通过归纳的方式...
关键词：软件验证 K-归纳法 不变式 谓词抽象 反例引导的抽象精炼 
葛梯尔型反例的谓词抽象式解答方案
《学术研究》2015年第11期25-30,共6页魏燕侠 
2013年度国家社科基金青年项目"形式知识论研究"(13CZX052);2012年度福建省教育厅A类人文社科项目"形式知识论"(JA12031S);2011年度福建省高校杰出青年科研人才培育计划项目"葛梯尔问题的逻辑分析"(11FJPY06)的阶段性成果
葛梯尔问题是当代知识论的核心问题,层出不穷的葛梯尔型反例使葛梯尔问题的解答蒙上了阴影。对葛梯尔型反例进行逻辑分析,体现了葛梯尔问题研究的最新动向。包括葛梯尔第一反例在内的一批葛梯尔型反例,是自然语言的辖域歧义导致的语言...
关键词：葛梯尔型反例 谓词抽象 语言辖域问题 
面向软件源程序的模型检验技术
《空间控制技术与应用》2015年第2期57-62,共6页李声涛 陈睿 顾斌 
国家自然科学基金资助项目(91118007)
模型检验技术作为一种有效的形式化方法,能够提供严格的软件质量保证.介绍了面向软件源程序的模型检验技术的工作流程,并在此基础上针对规约性质描述问题,提出一种与源代码独立的、语法简单易用的、符合程序员开发习惯的规约描述语言,...
关键词：软件分析 形式化方法 模型检验 源程序验证 谓词抽象 
谓词抽象和“弗雷格之谜”
《学术研究》2014年第10期23-28,159,共6页邓雄雁 秦波 胡泽洪 
国家社会科学基金项目"自由逻辑及其相关哲学问题研究"(13BZX068)的阶段性成果
弗雷格认为"相等"问题需要考虑涵义和意谓两个因素,这个问题包含相等的必然性、同一保真替换有效性和空词项三方面的问题。这些之所以成为问题,原因在于缺乏一个有效手段对"相等"的从言和从物形式进行区分,并误认为内涵和外延是截然对...
关键词：弗雷格 相等 从言模态 从物模态 谓词抽象 
不可满足子式在谓词抽象中的应用与分析
《计算机应用》2014年第A01期273-276,共4页张建民 黎铁军 张峻 庞征斌 李思昆 
国家863计划项目(2012AA01A301);国家自然科学基金资助项目(61103083;61133007)
随着软硬件设计的规模越来越大,功能越来越复杂,往往导致形式化验证出现"组合爆炸"问题,而谓词抽象方法是解决状态空间"组合爆炸"问题的重要技术之一。面向硬件的谓词抽象方法是不可满足子式的典型应用,通过求解不可满足子式,能够减少...
关键词：功能验证 形式化方法 谓词抽象 布尔可满足性 最小不可满足子式 
谓词抽象和模态谓词逻辑的合法性被引量：1
《世界哲学》2014年第2期139-145,共7页邓雄雁 胡泽洪 
国家社会科学基金项目"自由逻辑及其相关哲学问题研究"(13BZX068);广东省哲学社会科学规划学科共建项目"现代逻辑视野中的当代真理论"(GD11XZX01);广东省优长学科;特色学科建设专项资助课题"现代逻辑背景下的真理论研究"(2013YCTS10)资助
奎因对模态谓词逻辑的合法性持怀疑态度,他从逻辑角度论证了模态语境是指称不明的,同一替换原理和存在概括规则在模态语境中都是无效的,他的批评影响很大。但是,若在模态谓词逻辑中引入谓词抽象,它可以表达所有模态从言和从物命题,还能...
关键词：模态逻辑 谓词抽象 从言模态 从物模态 严格指示词 
基于谓词抽象的上期所异常交易监管应用研究
《计算机应用与软件》2013年第5期248-250,共3页柯莉珍 
对异常交易行为的监管是期货市场强化自律监管、完善监查规则体系、规范运行秩序的客观需要。创新性地对上海期货交易所异常交易监控的交易规则进行数学抽象,并在程序设计中运用形式化的自动推演思想,为今后期货交易规则制定的理论化,...
关键词：异常交易 程序化监管 汇总分析 谓词表达式 程序自动推演 
谓词抽象:一种新型语言辖域装置被引量：1
《科学技术哲学研究》2012年第5期47-52,共6页魏燕侠 
2011教育部人文社会科学研究青年项目(11YJC720044);2011年度福建省高校杰出青年科研人才培育计划项目(11FJPY06);2009年度福建省社会科学规划一般项目(2009B2051);华侨大学高层次引进人才项目(08BS501)
自然语言歧义所产生的哲学问题在语言哲学史上占据着重要位置。罗素的摹状词理论中包含着一种基于经典逻辑的语言辖域装置,它解决了"排中律失效"问题。作为一种基于量化模态逻辑的新型语言辖域装置,谓词抽象可以解决包括奎因的"指称晦...
关键词：谓词抽象 语言歧义 辖域装置 摹状词 
基于谓词抽象的测试用例约简生成方法被引量：10
《通信学报》2012年第3期35-43,51,共10页郭曦 张焕国 
国家自然科学基金资助项目(91018008;61003268;61173138);空天信息安全与可信计算教育部重点实验室开放基金资助项目(AISTC2008_01;AISTC2008Q02);湖北省自然基金资助项目(2009DBA429;2010CDB08601);中央高校基本科研业务费专项资金资助项目(3101038;115010)~~
针对大规模软件系统状态迁移数量庞大,容易导致状态空间爆炸的问题,提出一种基于谓词抽象的测试用例约简生成方法,该方法依据给定的谓词集合对软件系统的状态空间进行等价类划分,通过状态集合之间的映射得到约简的抽象状态,并以抽象状...
关键词：谓词抽象 状态约简 等价类划分 测试用例生成 
基于抽象和搜索空间划分的安全性判定方法被引量：1
《计算机科学》2011年第10期55-59,共5页王昌达 华明辉 周从华 宋香梅 鞠时光 
国家自然科学基金(60773049);江苏省自然科学基金(BK2007086);江苏省高校自然科学研究计划(07KJB520016);江苏省六大人才高峰项目(1631170006);江苏大学高级人才项目(07JDG053)资助
为满足访问控制策略安全性快速判定的要求,提出一种基于谓词抽象和验证空间划分的访问控制策略状态空间约减方法,将在访问控制策略原始状态机模型上的安全性分析工作转移到包含较少状态的抽象模型上,并进一步划分抽象模型的验证空间,以...
关键词：访问控制 谓词抽象 安全性分析 模型检测 可信评估 
全选清除导出
共3页<123>
检索报告 对象比较 聚类工具 使用帮助 返回顶部