形式化证明

作品数：37被引量：104H指数：6
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：左正康沈昌祥李益发王昌晶郁文生更多>>
相关机构：江西师范大学北京邮电大学解放军信息工程大学中国科学技术大学更多>>
相关期刊：《江西师范大学学报（自然科学版）》《计算机系统应用》《中国科技论文在线精品论文》《现代电子技术》更多>>
相关基金：国家自然科学基金江西省自然科学基金中央高校基本科研业务费专项资金中国博士后科学基金更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
面向无线传感器网络的认证密钥协商机制
《小型微型计算机系统》2024年第5期1204-1208,共5页李贵勇 张航 韩才君 李欣超 
教育部-中国移动科研基金项目(MCM201805-2)资助。
无线传感器网络(Wireless Sensor Networks,WSN)是物联网的重要组成部分,因为WSN能通过因特网将采集到的数据发送到云服务器.认证和密钥协商机制是一个重要的密码学概念,可以确保数据传输的安全和完整性.传感器节点是资源受限的设备,因...
关键词：无线传感器网络 认证和密钥协商 eCK模型 CDH假设 形式化证明 
作为数学革命的形式化证明
《自然辩证法研究》2024年第1期107-112,共6页杨帆 
中央高校基本科研业务费专项资金资助“面向机器定理证明的模糊逻辑研究”(3132022308)。
随着计算机科学的兴起,数学家可以通过计算机完成对数学定理的证明与验证,由此形成了形式化证明的相关领域。在形式化证明的助力下,诸多数学难题得以攻破,这无疑改变了传统数学实践的范式。然而,学界对于形式化证明所引发的认识论转向...
关键词：形式化证明 机器定理证明 数学革命 
基于Coq的杨忠道定理形式化证明被引量：1
《软件学报》2022年第6期2208-2223,共16页严升 郁文生 付尧顺 
国家自然科学基金(61936008)。
实现拓扑学定理的机器证明,是吴文俊院士生前的宿愿.杨忠道定理涉及一般拓扑学中的诸多基本概念,对深刻理解拓扑空间的本质有重要意义.该定理表明,拓扑空间中每一个子集的导集为闭集当且仅当此空间中的每一个单点集的导集为闭集,是一般...
关键词：COQ 形式化证明 公理化集合论 一般拓扑 拓扑空间 杨忠道定理 
二叉树队列关系问题非递归算法的推导及形式化证明被引量：2
《江西师范大学学报（自然科学版）》2022年第1期49-58,共10页左正康 方越 黄志鹏 黄箐 王昌晶 
国家自然科学基金(61862033,61902162);江西省教育厅科技重点课题(GJJ210307);江西省自然科学基金(20202BAB202015)资助项目.
该文对二叉树类问题进行分划,寻找其递推关系,并针对具有队列递推关系的一类问题,给出了其推导过程和形式化证明策略.再结合每个算法后置断言的不同,提出3种开发循环不变式的策略,并构造出该类问题的通用循环不变式模板.同时,发现该类...
关键词：二叉树队列递推关系 循环不变式 Dijkstra-Gries标准程序证明法 Apla到C++程序自动生成系统 非线性数据结构 
面向形式化证明的命令生成技术
《计算机系统应用》2022年第1期273-278,共6页莫广帅 熊焰 黄文超 
国家自然科学基金(61972369)。
随着软件规模的不断增大,软件安全问题日益严重.作为软件系统安全检测的有效手段,形式化证明旨在利用数学方法完成对软件属性的严格验证.常用的形式化证明方法利用模式匹配来进行定理证明,但存在策略生成不完备等缺陷.本文提出一种基于...
关键词：形式化证明 COQ 命令预测 LSTM 注意力机制 
图搜索问题算法推导及形式化证明
《江西师范大学学报（自然科学版）》2021年第6期642-651,共10页刘晓丹 胡颖 左正康 
国家自然科学基金(61862033,61762049,61902162);江西省教育厅科学技术研究(GJJ210307);江西省教育厅研究生创新基金(YC2021-S306);江西省自然科学基金(20202BABL202026,20202BABL202025,20202BAB202015)资助项目.
用非形式化方法解决图搜索问题规模受限,对于一些复杂问题难以保证其正确性.传统的形式化方法推导图搜索问题难以理解且不易于形式化证明,现有形式化方法对这类问题的解决方案较少,在保证可靠性和正确性方面有欠缺.该文通过对图搜索问...
关键词：图搜索问题 循环不变式 递归定义 形式化证明 
基于Coq的两个重要极限的形式化证明
《中国科技论文在线精品论文》2021年第2期177-186,共10页赵保强 于畅 郁文生 
数学机械化主要是利用计算机实现对数学定理的推理,形式化数学是数学机械化的重要内容.本文利用交互式定理证明工具Coq实现两个重要极限的形式化证明,其中主要包括集合、数列、函数、极限等概念的定义以及相关定理的证明.在此基础上建...
关键词：人工智能 极限 形式化验证 定理机器证明 级数 COQ 
基于属性基隐私信息检索的位置隐私保护方法被引量：10
《哈尔滨工程大学学报》2021年第5期680-686,共7页杜刚 张磊 马春光 张国印 
国家自然科学基金项目(61932005,U1936112);中国博士后基金项目(2019M661260);黑龙江省自然科学基金项目(YQ2019F018,LH2019F011).
针对基于位置服务隐私保护中以索引为主的隐私信息检索策略在处理时间和用户属性保护方面的不足,提出了一种属性基隐私信息检索的位置隐私保护方法。该方法基于属性基加密算法结合位置服务的本质特征,通过用户与位置服务器之间的两方秘...
关键词：基于位置服务 隐私保护 索引 隐私信息检索 属性基加密算法 秘密计算 零信息泄露 属性隐藏 形式化证明 
二叉树排序非递归算法推导及形式化证明被引量：6
《江西师范大学学报（自然科学版）》2020年第6期625-632,共8页左正康 方越 黄箐 廖云燕 王渊 王昌晶 
国家自然科学基金(61862033,61762049,61902162);江西省自然科学基金(20202BABL202026,2020BABL202025,20202BAB202015);国家留学基金(202008360094)资助项目.
非线性数据结构递归问题非递归算法的循环不变式的开发一直是形式化开发的难点.研究二叉树类非递归算法的推导及形式化证明方法,对二叉树排序算法进行推导,得出非递归Apla(Abstract Programming Language)算法及其精确而简单的循环不变...
关键词：二叉树类非递归算法 循环不变式 PAR平台 Dijkstra-Gries标准程序证明法 非线性数据结构 
基于区块链技术的RFID匿名认证协议被引量：1
《网络安全技术与应用》2020年第6期20-23,共4页庄园 甘勇 王冰丽 贺蕾 
广泛使用的无源RFID标签在计算能力和存储方面受限较多,这为RFID标签的安全认证问题带来了极大的挑战。为了保证通信各方隐私安全,同时抵抗不同类型的攻击,本文提出了一种全新的基于区块链技术的RFID标签匿名认证协议,协议使用哈希函数...
关键词：RFID 区块链技术 认证 GNY形式化证明 
全选清除导出
共4页<1234>
检索报告 对象比较 聚类工具 使用帮助 返回顶部