定理证明

作品数：1006被引量：857H指数：10
导出分析报告
相关领域：理学自动化与计算机技术更多>>
相关作者：关永施智平李晓娟张杰王国辉更多>>
相关机构：首都师范大学南京航空航天大学北京化工大学华东师范大学更多>>
相关期刊：更多>>
相关基金：国家自然科学基金国际科技合作与交流专项项目国家重点基础研究发展计划国家高技术研究发展计划更多>>
-
在结果中检索

检索结果分析

结果分析中...
选择条件：
  • 期刊=软件学报x
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
LLRB算法的函数式建模及其机械化验证
《软件学报》2024年第11期5016-5039,共24页左正康 黄志鹏 黄箐 孙欢 曾志城 胡颖 王昌晶 
国家自然科学基金(61862033,62262031);江西省自然科学基金(20212BAB202018);江西省教育厅科技重点项目(GJJ210307)。
基于机器定理证明的形式化验证技术不受状态空间限制,是保证软件正确性、避免因潜在软件缺陷带来严重损失的重要方法.LLRB(left-leaning red-black trees)是一种二叉搜索树变体,其结构比传统的红黑树添加了额外的左倾约束条件,在验证时...
关键词：LLRB 函数式建模 机械化验证 Isabelle定理证明器 二叉搜索树 
形式化方法与应用专题前言
《软件学报》2024年第9期4011-4012,共2页曹钦翔 宋富 詹乃军 
随着硬件运算速度变得越来越快、体系结构变得越来越复杂,软件的功能也变得越来越强大而复杂,如何开发可靠的软件系统,已经成为了一项巨大的挑战.形式化方法是利用数学理论与方法论证检验软件系统可靠性与安全性的方法,包括模型检验、...
关键词：形式化方法 软件系统 模型检验 运算速度 定理证明 体系结构 应用专题 理论与方法论 
基于交互式定理证明的并发程序验证工作综述
《软件学报》2024年第9期4069-4099,共31页王中烨 吴姝姝 曹钦翔 
并发程序与并发系统可以拥有非常高的执行效率和相对串行系统较快的响应速度,在现实中有着非常广泛的应用.但是并发程序与并发系统往往难以保证其实现的正确性,实际应用程序运行中的错误会带来严重的后果.同时,并发程序执行时的不确定...
关键词：并发程序验证 可线性化 上下文精化 程序逻辑 关系霍尔逻辑 
微内核操作系统互斥量模块功能正确性的形式化验证
《软件学报》2024年第9期4179-4192,共14页张林雁 李希萌 施智平 关永 曹钦翔 张倩颖 
国家自然科学基金(62002246,62272322,62272323,62372311,62372312,61902240)。
操作系统在许多安全攸关领域为软件系统提供关键性底层支撑,操作系统中一个微小的错误或漏洞都可能引起整个软件系统的重大故障,造成巨大经济损失或危及人身安全.为了减少此类安全事故的发生,对操作系统正确性进行验证十分必要.传统测...
关键词：互斥量 功能正确性 形式化验证 定理证明 Coq定理证明器 
共识协议的形式化验证研究现状与展望
《软件学报》2023年第11期4989-5007,共19页葛宁 贺俞凯 翟树茂 李晓洲 张莉 
国家重点研发计划(2018YFB1402700);国家自然科学基金(61902011);北京航空航天大学软件开发环境国家重点实验室开放课题(SKLSDE-2021ZX-01)。
分布式系统在计算环境中发挥重要的作用,其中的共识协议算法用于保证节点间行为的一致性.共识协议的设计错误可能导致系统运行故障,严重时可能对人员和环境造成灾难性的后果,因此保证共识协议设计的正确性非常重要.形式化验证能够严格...
关键词：共识协议 形式化验证 限界模型检测 定理证明 布尔表达式可满足性理论 可满足性模理论 
基于函数式语义的循环和递归程序结构通用证明技术
《软件学报》2023年第8期3686-3707,共22页李希萌 王国辉 张倩颖 施智平 关永 
国家重点研发计划(2019YFB1309900);国家自然科学基金(61876111,61877040,62002246);北京市教育委员会科技计划(KM201910028005,KM202010028010)。
各类安全攸关系统的可靠运行离不开软件程序的正确执行.程序的演绎验证技术为程序执行的正确性提供高度保障.程序语言种类繁多,且用途覆盖高可靠性场景的新式语言不断涌现,难以为每种语言设计支撑其程序验证任务的整套逻辑规则,并证明...
关键词：程序验证 大步操作语义 定理证明 Coq定理证明器 
约束求解与定理证明专题前言
《软件学报》2023年第8期3465-3466,共2页蔡少伟 陈振邦 王戟 詹博华 赵永望 
随着计算机系统在工业和生活中越来越广泛的应用,软件和硬件的可靠性受到越来越多的关注.形式化方法使用严格的数学语言对计算机系统建模,并在计算机的辅助下验证系统的正确性.与测试不同,形式化方法可以完全排除某些类型的错误.约束求...
关键词：形式化方法 定理证明 约束求解 符号执行 计算机系统 模糊测试 模型检测 系统安全 
基于精化的TrustZone多安全分区建模与形式化验证被引量：2
《软件学报》2023年第8期3507-3526,共20页曾凡浪 常瑞 许浩 潘少平 赵永望 
浙江省重点研发计划(2022C01165);国家自然科学基金(62132014);浙江省尖兵计划(2022C01045);中央高校基本科研业务费(NGICS)专项资金。
TrustZone作为ARM处理器上的可信执行环境技术,为设备上安全敏感的程序和数据提供一个隔离的独立执行环境.然而,可信操作系统与所有可信应用运行在同一个可信环境中,任意组件上的漏洞被利用都会波及系统中的其他组件.虽然ARM提出了S-EL...
关键词：可信执行环境 安全分区 定理证明 精化 安全性分析 
支持索引式的PPTL定理证明器的实现被引量：1
《软件学报》2022年第6期2172-2188,共17页王小兵 寇蒙莎 李春奕 赵亮 
国家自然科学基金(61672403,61972301);陕西省重点研发计划(2020GY-043,2020GY-210)。
定理证明是目前主流的形式化验证方法,拥有强大的抽象和逻辑表达能力,且不存在状态空间爆炸问题,可用于有穷和无穷状态系统,但其不能完全自动化,并且要求用户掌握较强的数学知识.含索引式的命题投影时序逻辑(PPTL)是一种具有完全正则表...
关键词：定理证明 COQ 索引式 命题投影时序逻辑 公理系统 
基于Coq的矩阵代码生成技术被引量：1
《软件学报》2022年第6期2224-2245,共22页麻莹莹 陈钢 
矩阵程序在智能系统中扮演着越来越重要的角色.随着矩阵应用的复杂性日益增加,生成正确矩阵代码的难度也在不断变大.并行硬件能够极大地提高矩阵运算的速度,然而,使用并行硬件进行编程以实现并行运算,需要编程人员在程序中描述功能以及...
关键词：定理证明 矩阵代码生成 形式化工程数学 高阶定理证明 COQ 
全选清除导出
共4页<1234>
检索报告 对象比较 聚类工具 使用帮助 返回顶部