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

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

矛盾体分离超演绎方法及应用

作为当前自动定理证明器中常用的推理机制,传统基于二元演绎超归结方法的推理过程限定每次有且只有2个子句参与演绎,这种分离的演绎步骤导致演绎缺失导向性和预判性,演绎效率有待提升。为了提升演绎效率,在理论上,针对传统的超归结方法引入多元演绎思想,提出矛盾体分离超演绎定义和方法,它具有多元性、动态性和导向性的演绎特性;在算法实现中,考虑子句参与演绎具有多元和协同特性,并灵活设定演绎的条件,提出一种具有回溯机制的矛盾体分离超演绎算法。将所提算法应用于Eprover3.1证明器,以国际自动定理证明器2023年竞赛例和TPTP(Thousands of Problems for Theorem Provers)问题库中难度系数为1的问题作为测试对象,在300 s内,应用所提算法的Eprover3.1证明器比原始Eprover3.1多证明了15个定理;当测试相同数量的定理时,所提算法的平均证明时间缩减了1.326 s,能够证明7个难度系数为1的定理。测试结果表明,所提算法能有效地应用于一阶逻辑自动定理证明,提升自动定理证明器的证明能力和效率。

微内核操作系统互斥量模块功能正确性的形式化验证

操作系统在许多安全攸关领域为软件系统提供关键性底层支撑,操作系统中一个微小的错误或漏洞都可能引起整个软件系统的重大故障,造成巨大经济损失或危及人身安全.为了减少此类安全事故的发生,对操作系统正确性进行验证十分必要.传统测试手段无法穷尽系统中的所有潜在错误,因而操作系统验证有必要使用具有严格数学理论基础的形式化方法.在操作系统中,互斥量可协调多任务对资源的访问,是一种常用的任务同步方式,其功能正确性对于保障多任务应用的正确性十分关键.基于定理证明方法,在交互式定理证明器Coq中对某抢占式微内核操作系统的互斥量模块进行代码级形式化建模,给出其接口函数的形式化规范,并实现这些接口函数的功能正确性验证.

基于二幂阶矩阵的量子中间表示与翻译

在两能级量子计算系统中,所有量子门、量子态和测量算子都可以表示为2的幂次方阶矩阵(简称二幂阶矩阵)的形式,而现有量子编程语言未考虑该特性。因此,提出一种二幂阶矩阵类型系统,并设计相应的量子中间表示。首先,在定理证明器Coq中利用递归对偶结构实现二幂阶矩阵系统,可以精确描述量子门、量子态和测量算子;其次,设计一套量子中间表示作为编程工具,可以自动将量子程序翻译为二幂阶矩阵表达式;最后,展示量子傅里叶变换的编写和翻译过程。二幂阶矩阵系统为基于定理证明器的量子编程语言提供了更精确、更简洁的类型系统,量子中间表示实现了从二幂阶矩阵到程序语言的过渡,提供了在二幂阶矩阵系统中编写量子程序的有效手段。

基于定理证明器的行波进位加法器开发以及新的芯片设计方法探索

数字芯片的规模已经进入几百亿晶体管的时代,传统的硬件设计方法难以应对日益复杂的电路需求,比如基于Verilog语言的硬件设计。针对这个问题,文章以行波进位加法器为例,探索基于交互式定理证明器Coq的芯片设计方法,该方法不仅在Coq中完成了加法器的RTL描述,而且进行了加法器的功能仿真、形式验证、Verilog代码生成、网表生成和网表仿真。这个案例在单一的编程平台里把RTL设计同前端EDA的主要流程整合在一起,虽然案例简单,但可以初步体现出基于Coq的芯片前端设计的可能性,并且希望能够从此出发探索出新的基于定理证明器的芯片设计流程。文章的主要技术路线是在Coq中开发芯片设计的抽象语法树,然后基于这个抽象语法树展开行波进位加法器的前端开发流程。实验结果表明,Coq在支撑芯片设计方面有巨大的潜力,并且基于定理证明器的验证是可以复用的,这有利于验证大规模的系统。尽管这一方法处于探索阶段,但它为未来的芯片前端设计提供了全新的思路,有希望发展成为一种新型的芯片前端设计方法。

可由用户持续发展的几何自动推理平台的推理算法

目前的几何定理证明器都不具有可持续性。提出一种结构具有一般性的知识表示和能够统一处理所有规则的推理算法,初步实现了可由用户持续发展的几何自动推理平台。该推理平台允许用户添加几何知识,如几何对象、谓词和规则,并可以综合使用多种推理算法,如前推搜索法和一部分面积法,它将更适合用于几何教学。

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

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

安全协议的形式化需求及验证

该文采用近世代数和时序逻辑的方法提出并描述了密码协议的形式化安全需求,并在AT模型的基础上加入信任和知识的非单调逻辑,建立了安全协议的计算模型。利用该计算模型对Denning_Sacco公钥协议进行了验证,发现了对此协议的重放攻击,并对协议进行了修改。

基于Isabelle定理证明器算法程序的形式化验证

形式化验证对保证软件的正确性和可靠性具有十分重要的意义。定理机械证明是形式化验证的一个重要研究领域,Isabelle系统是一个被广泛运用的定理证明辅助工具。本文在分析Dijkstra最弱前置谓词理论的基础上,根据PAR方法开发的算法程序循环不变式,提出了一种使用Isabelle定理证明器对算法程序进行机械验证的方法。该方法既克服了传统手工验证过程的繁琐性和易错性等缺点,又达到"提高验证效率和保证算法程序高可信"的目标,具有很好的实用价值。

面向计算机专业的数理逻辑实验课的教学改革

随着定理证明技术在国内科研院所、大专院校以及企业中的推广,在面向计算机专业的数理逻辑课程中开展基于定理证明器的实验课教学,可以引入更多计算的色彩,调动学生的学习兴趣,对推动数理逻辑教学改革有着积极的作用。

中介模态逻辑MS_4的表推演系统

中介逻辑是一个新的逻辑系统，该系统的创立有明显的哲学背景，自创立后得到了很大的发展。在数理逻辑以及计算机科学领域已发展了中介模态逻辑以及ＭＩＬＬ等中介程序计设语言，但对作为程序计设语言之逻辑基础之一的中介模态逻辑的自动推理理论与实现的研究还很不够。本文系统地讨论中介模态逻辑ＭＳ４的自动定理证明理论，构造了中介模态逻辑ＭＳ４的表推演系统。由于该系统采用＂与或树＂的表达方法，因而不产生＂遗忘问题＂；又由于设置的μ＇扩展规则有效地限制了＂秩＂的递增次数，从而保证了该系统的完备性。本文第一部分给出了中介模态逻辑ＭＳ４的表推演系统及一个应用实例，第二部分证明了该系统的可靠性与完备性定理。

安全协议分析的界——综合模型检查与Strand Spaces(英文)

Strand Spaces是一种用于分析安全协议的机器证明方法.简要介绍了 Strand Spaces的基本特点,分析了其优劣,提出了构造协议的理想子环的算法,并以此来约束协议入侵者的能力和协议并行运行的次数.将模型检查与 Strand Spaces结合在一起,提出了一种综合分析方法来验证协议的安全特性,该方法可充分发挥模型检查与 Strand Spaces二者的优势.

一个用于指针程序验证的自动定理证明器的设计与实现

对高可信软件需求的增加使得指针程序的验证成为近期的研究热点.指针逻辑作为Hoare逻辑的扩展,可以对指针程序进行精确的分析.介绍一个针对指针逻辑的自动定理证明器的设计和实现,描述了一些算法.实验结果表明,该定理证明器可以完全自动的证明用类C语言编写的关于单链表,双链表和二叉树的指针程序的验证条件,并生成机器可检查的证明.

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

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

用于指针逻辑的自动定理证明器(英文)

提出了一种为指针逻辑设计定理证明器的新技术,该项技术主要是基于变换和替代,已在APL的工具中得以实现.APL自动定理证明器是完全自动的,且其产生的证明可以被有效地记录和检验.已使用关于单链表、双链表和二叉树的指针程序测试了该自动定理证明器.

定理证明辅助工具PVS剖析

ＰＶＳ是斯坦福研究机构开发的强大的规约、验证系统，它的适用领域广泛。在概要介绍ＰＶＳ的构成、功能后，着重分析了ＰＶＳ的规约语言、验证系统的特点，以及使得ＰＶＳ灵活、强大的设计决策和内在机制．

基于复数法的几何定理可读机器证明

已有的机器证明方法在处理一些涉及大规模符号运算的几何问题时,常因算法复杂度过高或机器能力的限制,有时并不能在合理时间内实现可读机器证明.故提出了复数法这一新的几何定理机器证明算法,并选用符号计算功能较为强大的软件Mathematica创建了新证明器CNMP(complex number method prover).新提出的复数法能有效地解决构造型几何命题,对用于测试与评价几何定理证明器性能的综合性平台TGTP(thousands of geometric problems for geometric theorem provers)上的180个几何问题的实验结果表明,CNMP的解题能力与运行效率均令人满意.尤其是对于一些具有相当难度的几何定理,如五圆定理、Morley定理、Lemoine圆定理、Thebault定理、Brocard圆定理等,CNMP均能在短时间内给出可读机器证明.

一种基于分离逻辑的块云存储系统验证工具

云存储技术目前被广泛应用于人们的生产与生活中.验证云存储系统中管理程序的正确性,能够有效地提高整个系统的可靠性.块云存储系统(CBS)具有最接近底层的存储架构.运用交互式定理证明器Coq,实现了一种辅助验证工具,用于分析和验证CBS中管理程序的正确性.基于分离逻辑的思想,对工具中证明系统的实现主要包括:首先,将CBS抽象为两层堆结构,定义建模语言形式化表示CBS的状态和管理程序;其次,定义描述CBS状态性质的堆谓词,并说明堆谓词间的逻辑关系;最后,定义描述程序行为的CBS分离逻辑三元组,以及制定验证三元组所需的推理规则.此外,还引入了几个证明实例,以此展示工具对实际CBS管理程序表示和推理的能力.

汇编级顺序语句块的自动形式化规约及其验证

软件的形式化验证是保障软件可证明性、可靠性和安全性的重要手段,但传统形式化验证脚本的生成过程复杂且需要形式化验证专家的大量手工验证。为提高证明效率,构建一种自动证明模型,并在此基础上提出语义自动规约算法以及对所规约的语义自动生成证明脚本的算法。利用C++和Python并通过交互式定理证明器Isabelle 2017在基准数据中随机选择10个程序进行测试,结果表明,与完全人工操作相比,该算法具有较高的验证效率,可实现顺序语句块的自动化规约与验证。

基于Coq的命令式语言编译器机械验证的研究与实现

软件的可靠性和可信性越来越受到人们的关注,而编译器作为软件开发的基础,其正确性的验证一直都是个重要且迫切的问题.设计和实现一个小型命令式语言IMP的编译器,该编译器将IMP源代码转换成定理证明器Coq接受的函数式语言表示形式的代码,通过语义分析得到IMP目标代码,在堆栈中执行得到结果.本文的重点是使用交互式定理证明器Coq机械验证函数式语言表示形式的源代码编译执行前后的属性和行为均保持一致.本文的工作为使用堆栈的编译器和其他软件系统的机械化形式验证提供了一种新的思路和方法.