检索结果-南通市图书馆

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

LLRB算法的函数式建模及其机械化验证

软件学报 2023年

作者：左正康黄志鹏黄箐孙欢曾志城胡颖王昌晶江西师范大学计算机信息工程学院江西师范大学数字产业学院

基于机器定理证明的形式化验证技术不受状态空间限制,是保证软件正确性、避免因潜在软件缺陷带来严重损失的重要方法. LLRB (left-leaning red-black trees)是一种二叉搜索树变体,其结构比传统的红黑树添加了额外的左倾约束条件,在验证... 详细信息

基于机器定理证明的形式化验证技术不受状态空间限制,是保证软件正确性、避免因潜在软件缺陷带来严重损失的重要方法. LLRB (left-leaning red-black trees)是一种二叉搜索树变体,其结构比传统的红黑树添加了额外的左倾约束条件,在验证时无法使用常规的证明策略,需要更多的人工干预和努力,其正确性验证是一个公认的难题.为此,基于二叉搜索树类算法isabelle验证框架,对其附加性质部分进行细化,并给出具体化的验证方案.在isabelle中对LLRB插入和删除操作进行函数式建模,对其不变量进行模块化处理,并验证函数的正确性.这是首次在isabelle中对函数式LLRB插入和删除算法进行机械化验证,相较于目前LLRB算法的Dafny验证,定理数由158减少到84,且无需构造中间断言,减轻了验证的负担;同时,为复杂树结构算法的函数式建模及验证提供了一定的参考价值.

关键词： LLRB 函数式建模机械化验证 Isabelle定理证明器二叉搜索树

基于isabelle的DFS算法的自动验证

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

基于Isabelle的DFS算法的自动验证

作者：谌冬云江西师范大学

学位级别：硕士

形式化方法以严格的数学化和机械化方法为基础来规约、构建和验证计算系统,是改善和确保计算系统质量的重要方法,其模型、技术和工具已延伸成为计算思维的重要载体。形式化方法中,形式化推导是通过对问题程序规约进行精确变换,最终得到... 详细信息

形式化方法以严格的数学化和机械化方法为基础来规约、构建和验证计算系统,是改善和确保计算系统质量的重要方法,其模型、技术和工具已延伸成为计算思维的重要载体。形式化方法中,形式化推导是通过对问题程序规约进行精确变换,最终得到算法程序。形式化验证是在对软件进行规约的基础上,验证软件是否具有所期望的性质。软件形式化方法使软件系统的描述更加精确,以减少可能的错误所带来的问题,提高软件的可靠性。图结构在现实生活中应用非常广泛,图的数据结构广泛应用在公路运输网络、地铁线路网络、网络节点优化等生活中的很多领域,另外计算机系统中的状态执行等也是基于图数据结构的。因此,图的深度优先遍历算法在现代的各种软件中应用十分频繁,这些软件的可靠性的高低很大程度取决于图的深度优先算法是否正确完备。深度优先算法的可靠性验证使用传统的手工推导来验证已经不能满足我们的需要了,数学定理证明工具isabelle与软件形式化方法的结合既可以适应日益繁琐的软件验证,又可以避免手工推导验证所带来的失误。isabelle是一种通用的且支持高阶逻辑的交互式定理证明器。它允许以正式语言表达数学公式,并提供用于在逻辑演算中证明这些公式的工具。主要应用是数学证明的形式化,尤其是形式化验证,其中包括证明计算机硬件或软件的正确性以及证明计算机语言和协议的特性。本文研究的内容主要是深入了解isabelle系统的验证原理和逻辑结构,探索将形式化方法与Isabelle定理证明器相结合应用于实际生产,在对比形式化方法中的几种验证方法的优缺点后,选择使用Dijkstra最弱前置谓词方法作为验证方法。为了实现对深度优先遍历算法的验证,本文对isabelle系统的规则库中加入了图的定义、深度优先遍历算法及其相关引理。并且结合Dijkstra最弱前置谓词方法完成了对图的深度优先遍历算法进行自动化验证。这些工作确保了深度优先遍历算法的可靠性和简化了手工推导验证的繁琐程度。扩充的isabelle类型库为以后的研究者丰富了图结构的定义。将形式化方法与证明工具相结合一定程度上会促进形式化方法应用到实际生产中。

关键词：形式化方法自动化验证 Isabelle定理证明器深度优先搜索算法

算法的形式化推导与基于isabelle的自动化验证

同方学位论文库评论

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

江西师范大学学报（自然科学版） 2018年第4期42卷 379-383页

作者：齐蕾蕾杨庆红游颖江西师范大学计算机信息工程学院江西南昌330022

可信软件的不断发展进一步推动了形式化方法的深入研究.结合实际应用中的2个问题,采用基于递推关系的算法形式化方法,演示了算法的形式化推导过程,并运用Isabelle定理证明器结合Dijkstra最弱前置谓词方法,对得到的算法程序进行了自动化... 详细信息

可信软件的不断发展进一步推动了形式化方法的深入研究.结合实际应用中的2个问题,采用基于递推关系的算法形式化方法,演示了算法的形式化推导过程,并运用Isabelle定理证明器结合Dijkstra最弱前置谓词方法,对得到的算法程序进行了自动化验证,避免了手工验证过程繁琐和易出错等问题.研究表明:基于递推关系的算法形式化方法不仅可以提高开发算法的效率,而且通过数学变换保证推导过程的正确性,从而有效保证了算法和程序的正确性.

关键词：形式化方法 Isabelle定理证明器自动化验证形式化推导

维普期刊数据库

在线全文

学校读者我要写书评

暂无评论

程序求精新策略及自动验证方法研究

郑州大学学报（理学版） 2022年第5期54卷 1-7页

作者：左正康黄志鹏黄箐王渊王昌晶江西师范大学计算机信息工程学院江西南昌330022 江西师范大学软件学院江西南昌330022

传统的程序求精策略无法求精至可执行程序,且存在验证的可信度低和自动化程度不高的问题。针对上述问题,提出一种较完整的程序求精策略并给出自动验证方法。使用递归定义函数技术刻画问题规约,基于Morgan精化规则程序求精至IMP程序,并... 详细信息

传统的程序求精策略无法求精至可执行程序,且存在验证的可信度低和自动化程度不高的问题。针对上述问题,提出一种较完整的程序求精策略并给出自动验证方法。使用递归定义函数技术刻画问题规约,基于Morgan精化规则程序求精至IMP程序,并使用验证条件生成器(verification condition generator,VCG)自动生成验证条件,通过Isabelle定理证明器验证IMP程序的正确性,最后利用开发平台自动生成C++可执行程序。以最长标志基因序列问题为实例进行程序求精和自动验证,检验了所提策略的有效性。该策略提高了算法程序开发的正确性,减轻了传统验证烦琐的工作量。

关键词：程序求精自动验证 Isabelle定理证明器 Morgan精化规则

维普期刊数据库