国家自然科学基金(90818018)

作品数：4被引量：23H指数：3
导出分析报告
相关作者：何炎祥李清安吴伟江南刘陶更多>>
相关机构：武汉大学湖北工业大学更多>>
相关期刊：《计算机研究与发展》《软件学报》《计算机工程与科学》《计算机科学》更多>>
相关主题：Λ演算机械化类型化消解定理证明更多>>
相关领域：自动化与计算机技术更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-4
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
机械化定理证明研究综述被引量：13
《软件学报》2020年第1期82-112,共31页江南 李清安 汪吕蒙 张晓瞳 何炎祥 
国家自然科学基金(90818018,91018009,61170022,91118003,61373039);华为技术有限公司合作项目(YB2015090035);湖北工业大学校博士科研启动基金(BSQD2017043)。
随着现代社会计算机化程度的提高,与计算机相关的各种系统故障足以造成巨大的经济损失.机械化定理证明能够建立更为严格的正确性,从而奠定系统的高可信性.针对机械化定理证明的逻辑基础和关键技术,详细剖析了一阶逻辑和基于消解的证明...
关键词：定理证明 证明助手 消解 自然演绎 类型化的λ演算 编程逻辑 求精 
程序的动态完整性:模型和方法被引量：3
《计算机研究与发展》2012年第9期1874-1882,共9页吴昊 毋国庆 
国家自然科学基金项目(90818018);国家自然科学基金重点项目(91118003)
在信息安全和可信计算中,程序的动态完整性是一个重要问题,特别是无线传感器网络、云计算平台等这一类开放松耦合环境下,怎样度量程序行为的动态完整性的问题尤为突出.基于硬件的可信计算技术和代码证实技术等都没有解决具体行为的动态...
关键词：可信软件 动态完整性模型 程序行为 编译器辅助 代码证实 
基于压缩的代码保护的低开销策略
《计算机科学》2011年第11期119-122,共4页陈勇 何炎祥 石谦 吴伟 李清安 
国家自然科学基金可信软件重大研究计划(90818018)资助
利用压缩算法及C语言编译器辅助分析,提出了一种用于代码保护的低开销策略。设计了一种基于C语言安全漏洞的安全级别模型,它对不同安全级别的代码采用不同的保护策略,以减少保护开销。同时设计了一种分块二进制压缩算法(BCC压缩算法),...
关键词：代码安全保护 安全模型 压缩算法 低存储容量 
可信编译器关键技术研究被引量：7
《计算机工程与科学》2010年第8期1-6,35,共7页何炎祥 刘陶 吴伟 
国家自然科学基金可信软件重大研究计划资助项目(90818018)
软件的可信性很大程度上依赖于程序代码的可信性。影响软件可信性的主要因素包括来自软件内部的代码缺陷、代码错误、程序故障以及来自软件外部的病毒、恶意代码等,因此从代码角度来保证软件的可信性是实现可信软件的重要途径之一。编...
关键词：可信编译 代码可信赖性 词法分析 微型编译器 
全选清除导出
共1页<1>
检索报告 对象比较 聚类工具 使用帮助 返回顶部