ISABELLE

作品数：14被引量：37H指数：4
导出分析报告
相关领域：自动化与计算机技术艺术更多>>
相关作者：钱振江黄皓游珍刘苇薛锦云更多>>
相关机构：江西师范大学南京大学中国科学院软件研究所常熟理工学院更多>>
相关期刊：《郑州大学学报（理学版）》《东方电影》《计算机学报》《计算机工程与设计》更多>>
相关基金：国家自然科学基金国家高技术研究发展计划江苏省“六大人才高峰”高层次人才项目江苏省高校自然科学研究项目更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
生物序列比对动态规划算法的统一形式化构造与Isabelle验证
《计算机研究与发展》2025年第1期119-131,共13页石海鹤 蓝孙文 刘日明 石海鹏 王岚 钟林辉 
国家自然科学基金项目(62062039)。
序列比对是生物序列分析中的一个经典问题,旨在找出序列之间的相似性,它对于发现生物序列中的功能、结构和进化信息都具有重要的意义.该问题可分为双序列比对和多序列比对2类,现有工作多针对特定算法展开,没有设计通用的求解方法;此外,...
关键词：序列比对 PAR方法 形式构造 Isabelle定理证明器 
LLRB算法的函数式建模及其机械化验证
《软件学报》2024年第11期5016-5039,共24页左正康 黄志鹏 黄箐 孙欢 曾志城 胡颖 王昌晶 
国家自然科学基金(61862033,62262031);江西省自然科学基金(20212BAB202018);江西省教育厅科技重点项目(GJJ210307)。
基于机器定理证明的形式化验证技术不受状态空间限制,是保证软件正确性、避免因潜在软件缺陷带来严重损失的重要方法.LLRB(left-leaning red-black trees)是一种二叉搜索树变体,其结构比传统的红黑树添加了额外的左倾约束条件,在验证时...
关键词：LLRB 函数式建模 机械化验证 Isabelle定理证明器 二叉搜索树 
程序求精新策略及自动验证方法研究被引量：3
《郑州大学学报（理学版）》2022年第5期1-7,共7页左正康 黄志鹏 黄箐 王渊 王昌晶 
国家自然科学基金项目(61862033,61902162);江西省自然科学基金项目(20202BAB202015);江西省教育厅科技重点项目(GJJ210307)。
传统的程序求精策略无法求精至可执行程序,且存在验证的可信度低和自动化程度不高的问题。针对上述问题,提出一种较完整的程序求精策略并给出自动验证方法。使用递归定义函数技术刻画问题规约,基于Morgan精化规则程序求精至IMP程序,并...
关键词：程序求精 自动验证 Isabelle定理证明器 Morgan精化规则 
Automatic Algorithm Programming Model Based on the Improved Morgan's Refinement Calculus被引量：5
《Wuhan University Journal of Natural Sciences》2022年第5期405-414,共10页ZUO Zhengkang HU Ying HUANG Qing WANG Yuan WANG Changjing 
Supported by the National Natural Science Foundation of China(61862033,61902162);Key Project of Science and Technology Research of Department of Education of Jiangxi Province(GJJ210307);Postgraduate Innovation Fund Project of Education Department of Jiangxi Province(YC2021-S306)。
The automatic algorithm programming model can increase the dependability and efficiency of algorithm program development,including specification generation,program refinement,and formal verification.However,the existi...
关键词：automatic algorithm programming model program refinement VCG ISABELLE Morgan’s refinement calculus 
伊莎贝拉·于佩尔Isabelle Huppert我不知道如何沉默
《东方电影》2019年第1期92-95,共4页甘琳 
“除了当演员,我什么都不会”,表演给予了伊莎贝拉·于佩尔最大程度的自由。并且,这是一种属于聪明人的自由,作为角色的于佩尔不知道如何沉默,而作为演员的于佩尔在表演结束之后,随即又会变得沉默,因为她知道电影不能和生活较劲。
关键词：沉默 贝拉 人的自由 演员 表演 电影 
算法的形式化推导与基于Isabelle的自动化验证被引量：2
《江西师范大学学报（自然科学版）》2018年第4期379-383,共5页齐蕾蕾 杨庆红 游颖 
国家自然科学基金(61363013)资助项目
可信软件的不断发展进一步推动了形式化方法的深入研究.结合实际应用中的2个问题,采用基于递推关系的算法形式化方法,演示了算法的形式化推导过程,并运用Isabelle定理证明器结合Dijkstra最弱前置谓词方法,对得到的算法程序进行了自动化...
关键词：形式化方法 Isabelle定理证明器 自动化验证 形式化推导 
微内核架构文件系统的形式化设计与验证方法研究被引量：4
《小型微型计算机系统》2013年第10期2261-2266,共6页钱振江 唐洪英 李康杰 黄皓 宋方敏 
国家"八六三"高技术研究发展计划项目(2011AA01A202)资助;国家自然科学基金创新研究群体基金项目(60721002)资助;江苏省"六大人才高峰"高层次人才项目(2011-DZXX-035)资助;江苏省高校自然科学基金项目(12KJB520001)资助
文件系统作为数据存储和管理的功能模块,其正确性是操作系统安全性的重要方面.采用形式化方法对微内核架构文件系统进行设计,使用操作系统对象语义模型(OSOSM)框架提出微内核架构文件系统的状态自动机模型,并依此描述系统调用的功能语...
关键词：文件系统 微内核架构 形式化设计 形式化验证 正确性断言 ISABELLE HOL 
操作系统对象语义模型(OSOSM)及形式化验证被引量：11
《计算机研究与发展》2012年第12期2702-2712,共11页钱振江 刘苇 黄皓 
国家"八六三"高技术研究发展计划基金项目(2011AA01A202);江苏省科技支撑计划基金项目(BE2008124);国家自然科学基金创新研究群体项目(60721002);江苏省"六大人才高峰"高层次人才项目(2011-DZXX-035);江苏省高校自然科学研究项目(12KJB520001)
操作系统的复杂性使得其安全性问题日益突出.有不少的研究工作采用形式化的方式对现有的操作系统进行了正确性的验证,这些工作主要是采用程序形式逻辑验证代码级的功能实现性.从系统设计的角度,以高阶逻辑和类型论为基础,提出了操作系...
关键词：操作系统对象 语义模型 形式化设计 安全性验证 Isabelle定理证明 
HybridHP:一种轻型的内核完整性监控方案及其形式化验证被引量：2
《计算机学报》2012年第7期1462-1474,共13页钱振江 刘苇 黄皓 
国家"八六三"高技术研究发展计划项目基金(2007AA01Z409);江苏省科技支撑计划自然科学基金(BE2008124);江苏省"六大人才高峰"高层次人才项目(2011-DZXX-035)资助~~
虽然传统的虚拟化监控方法可以在一定程度上保障操作系统安全.然而,虚拟监控器VMM中管理域Domain0的存在以及操作系统级的切换所带来的性能损失是很多具有大型应用的操作系统所不能接受的.注重硬件虚拟化技术的监控能力而摒弃其不必要...
关键词：硬件虚拟化 内核完整性 安全监控 安全攻击 Isabelle形式化验证 
基于Isabelle定理证明器算法程序的形式化验证被引量：10
《计算机工程与科学》2009年第10期85-89,共5页游珍 薛锦云 
国家自然科学基金资助项目(60573080,60773054);科技部国际科技合作资助项目(2008DFA11940)
形式化验证对保证软件的正确性和可靠性具有十分重要的意义。定理机械证明是形式化验证的一个重要研究领域,Isabelle系统是一个被广泛运用的定理证明辅助工具。本文在分析Dijkstra最弱前置谓词理论的基础上,根据PAR方法开发的算法程序...
关键词：形式化验证 定理机械证明 Dijkstra最弱前置谓词理论 PAR方法 算法程序 定理证明器 
全选清除导出
共2页<12>
检索报告 对象比较 聚类工具 使用帮助 返回顶部