随着现代社会计算机化程度的提高,与计算机相关的各种系统故障足以造成巨大的经济损失.机械化定理证明能够建立更为严格的正确性,从而奠定系统的高可信性.针对机械化定理证明的逻辑基础和关键技术,详细剖析了一阶逻辑和基于消解的证明技术、自然演绎和类型化的
Modern society is now being increasingly computerized. Computer-related failures could result in severe economic loss. Mechanized theorem proving is an approach to ensuring stricter correctness, and hence high trustworthiness. First, the logical foundations and key technologies of mechanized theorem proving are discussed. Specifically, first-order logic and resolution-based technology, natural deduction and Curry-Howard correspondence, three logics of programming including first-order programming logic and its variant, FloydHoare logic, and logic for computable functions, hardware verification technology based on higher-order logic, and program constructions and refinement are analyzed, as well as the relationship and evolvement between them. Then key design features of the mainstream proof assistants are compared, and the development and implementation of several representative provers are discussed. Next their applications in the fields of mathematics, compiler verification, operating-system microkernel verification, and circuit design verification are analyzed. Finally, mechanized theorem proving is summarized and challenges and future research directions are put forward.
计算机已经渗透到社会生产和人类生活的方方面面, 与计算机相关的各种故障足以造成巨大的经济损失. 2017年, 全球爆发的勒索病毒(WannaCry)源于Windows操作系统的漏洞(MS17-010);早在1994年, 奔腾处理器的浮点除运算错误使得英特尔公司不得不召回成百上千万芯片, 损失约4.5亿.更为严格的研发方法, 能够避免许多这样的错误.在这些方法中, 机械化定理证明是被学术界广泛认可的形式验证技术[
机械化定理证明是指使用计算机, 以定理证明的方式对数学定理或计算机软、硬件系统进行形式验证, 是人工智能(artificial intelligence, 简称AI)的一种体现.Leibniz早在17世纪时就形成了由机器证明定理的思想, 然而直到19世纪末现代逻辑的创立和发展, 以及20世纪40年代计算机的出现, 才使得这一设想的实现具有了现实可能性[
始于20世纪50年代和60年代, 机械化定理证明围绕计算机如何高度自动化地完成证明而展开.受当时倡导的人工智能潜能的影响, 自动定理证明(automated theorem proving, 简称ATP)技术的研究经历了一段炽热的研发期, 也取得了许多具有影响力的成果; 但是随着新问题、新技术和新思想的到来, 完全自动定理证明的研究渐入停滞期, 对于大多数有意义的数学定理或计算机系统的正确性, 交互式地进行证明可能是唯一可行的工作方式[
交互式定理证明(interactive theorem proving, 简称ITP)在20世纪60年代开始呈现, 交互式定理证明工具也称为证明助手(proof assistant).交互式意味着用户能够引导证明过程, 在这个过程中, 用户使用某种语言编写证明纲要(outline); 证明助手自动填充证明的细节, 并检查证明, 最终机器完成整个形式证明.这种证明纲要的思想最初体现在Wang于1960年的著作中[
自动定理证明最初旨在证明数学定理.不过, McCarthy同时指出:计算机能够检查的不仅仅是数学证明, 而且还包括复杂工程系统以及计算机程序是否符合它们的规范.事实正是如此, 从20世纪60年代晚期开始, 人们认识到许多其他问题, 譬如程序属性、专家系统和集成电路设计相关的许多问题等, 都可以表示为定理, 而由自动定理证明工具予以解决[
http://isabelle.in.tum.de/)、Coq(https://coq.inria.fr/)、HOL4(https://hol-theorem-prover.org/)、ACL2(http://www.cs.utexas.edu/users/ moore/acl2/)等.经过许多年的努力, 分别在Coq和Isabelle/HOL的支持下, 出现了首个验证的C优化编译器, 称为CompCert[
这些研究结果究竟是如何取得的?19世纪末, 德国哲学家、逻辑学家及数学家Frege试图证明“所有数学都可归为逻辑”, 结果创立了谓词逻辑; 20世纪, 德国数学家Hilbert试图证明数学是没有矛盾的, 他创建了现代证明理论; 荷兰数学家和哲学家Brouwer同样为了研究数学基础而开创了直觉主义的数学哲学[
本文第1节阐述与机械化定理证明紧密相关的概念和理论、主流或具有持续影响力的技术, 并剖析它们之间的联系以及变迁发展.第2节分析、比较各类证明助手的特点、开发和实现.第3节讨论它们在数学和计算机领域的应用现状, 并对编译器验证和操作系统微内核验证进行了详细分析.最后对机械化定理证明进行总结, 并提出面临的挑战和未来研究方向.
本节从一阶逻辑(first-order logic)和基于消解(resolution-based)的证明技术开始论述, 这是机械化定理证明研究得最久并仍然活跃的自动定理证明领域.然后, 论述将自然演绎和类型理论关联起来的Curry-Howard同构(correspondence), 它是当前以类型论为基础的证明助手的理论基石.接下来, 针对被广泛研究的程序的机械化验证, 讨论该领域主要使用的3种编程逻辑(logics of programming)和相关的编程语言语义(semantics).之后, 阐述在当时相当激进但却获得成功的基于高阶逻辑(higher-order logic)的硬件验证.最后讨论了程序构造(program construction)和求精(refinement)的方法.
自动定理证明要解决的主要问题是:
1) 知识如何展现?即用什么语言表述定理;
2) 如何由已有知识推导得到新的知识?即研究由已有定理(或公理)推出新定理的推理规则;
3) 如何找到证明, 即控制推理规则的使用.
自动定理证明最初使用相对简单的命题逻辑语言, 但是命题逻辑所能表述的定理太具限制性.相比而言, 一阶谓词逻辑(简称一阶逻辑)具有更强的表述力, 并具有理论上的完备性, 自动定理证明转而采用一阶逻辑.
第2)和第3)两个问题的解决相对更困难一些:数学家们或者人类在证明定理时, 人脑存储了许多已有知识.通常, 经验、洞察力、甚至直觉对完成定理的证明也起了很大作用; 开发自动定理证明工具需要找到适合机器推理的方法.Prawitz首次提出了通过计算进行合一(unification)的置换方法[
基于消解的证明技术迅速成为了广被研究的主题.大量研究开始深入探索启发式策略, 用来控制消解, 以减少证明搜索空间.许多启发式策略是领域特定的, 譬如适合平面几何的策略并不适合群理论.一些研究赞成更为通用的启发式策略, 将策略实现为作用在证明机制上的限制[
[
http://vprover.org), 它的研究始于1994年, 已连续多年获得由自动推理大会承办的自动定理证明工具竞赛的FOF(first-order formulas)组和CNF(first-order problems in conjunctive normal form)/MIX组的冠军.]]>
http://www.nuprl.org)和PVS(http://pvs.csl.sri.com)等的实现语言就是Lisp方言Common Lisp.]]>
基于消解的证明技术使用的是反驳法, 譬如, 如果要证明“由
自然演绎系统通常并不否定待证明定理, 它力图自然地、像人类思考那样进行推理.自然演绎系统具有许多推理规则, 它们和简单类型理论的类型规则之间存在着对应关系.Curry-Howard同构的发现以及扩展, 使得逻辑学家和计算机科学家基于证明和程序之间的对应关系而开发出了强大的类型理论以及相应的证明助手.
Hilbert于1920年启动了称为“Hilbert’s program”的研究计划, 目标是证明数学是一致的(consistent):所有数学都可由正确选择的一套公理系统而推得.然而, Gödel的不完备性定理被广泛认为宣告了Hilbert研究计划的失败.尽管如此, Hilbert创立了现代证明理论.在他的演绎推理系统中, 公理定义了大多数逻辑操作符的语法, 而仅有一条称为肯定前件式的推理规则, 这使得有些公理看起来令人生畏, 譬如((
Hilbert公理系统中的命题形如⊦
一个根岑风格的自然演绎系统(命题逻辑)
A natural deduction system of Gentzen style (propositional logic)
Gentzen的初始动机是为了证明数论的一致性.为实现这个目标, 他提出了称为“子公式属性(subformula property)”的概念, 即“任何形如
即“cut”掉了
这种简化的证明更易于机器推理.sequent推理演算系统事实上提供了一个方便的工具, 用于设计证明搜索算法, 该算法应用推理规则, 后向证明定理.Gentzen证明了一阶经典逻辑和直觉主义逻辑的sequent推理演算满足子公式属性, 并证明了具有一个无限归纳规则的算术公理系统的一致性.但是, 他不能证明形如Γ⊦
自然演绎系统具有大量的推理规则, 控制这些规则的使用, 是实现机械化推理的重要手段.譬如, 对于
机器证明
A roundabout mechanical proof of
从
A simple mechanical proof of
Church于1940年提出类型化的
最具有影响力的简单类型理论就是Church的类型化
其中, 符号⇒的意思是“归约为”.
为使得
在
类型化的
Church类型化
A fragment of Church's typed
类型论并未受到数学家们的欢迎, 但是通过Church的简单类型理论, 它得到了计算机科学家们的推崇:类型化的
相比集合论, 类型论在机械化解决许多问题方面更具有优势.譬如, 在集合论中可以书写被类型论视为不合法的各种表达式, 数学家们能从直觉上拒绝它们.但是操纵这些数学表达式的计算机并不具备这样的直觉, 如果不以某种策略方式告诉计算机区分不同类型的数学对象, 计算机的处理是相当低效的.此外, 自动推理系统中的一个基本操作是找到变量的合适置换, 区分不同实体的类型, 避免了大量无用搜索.
近些年来, 普林斯顿高等研究院(Institute for Advanced Study in Princeton)着手探究一种基于依赖类型的更复杂的类型论, 即同伦类型理论(homotopy type theory)[
由
直觉主义指的是Brouwer所代表的数学哲学思想.为解决朴素集合论中的悖论问题, Brouwer提出了与主流数学界完全不同的观点:悖论的存在说明了经典数学本身存在问题, 而不是因为数学家们在证明数学没有矛盾的方法上出了问题, 数学必须重新构建, 因此产生了直觉主义的算术、代数、集合论等等.Brouwer认为, 数学是人的思维活动, 数学由这样的思维活动一个接一个地归纳构造出来, 任何不能构造出来的东西都不属于数学.因此, 数学直觉主义哲学也称为构造主义数学.直觉主义拒绝排中律, 这在当时是一个相当尖锐的观点, 也因此没有得到主流数学的青睐.但是, 其“构造”的思想建立了直觉主义逻辑与计算之间的联系.
Gentzen的自然演绎在1934年发表, 但他不能简化自然演绎的证明; Church类型化的
证明
A proof of
进一步考虑, 根据
因此, 项的归约对应着证明的简化; 并且, 项的归约不会改变类型.
在“命题即类型”下, 定理的证明过程是高度构造的.证明一个定理就是构造出给定类型的项, 证明规范化成了计算, 证明检查对应于类型检查.Curry-Howard同构为许多主流证明助手的开发奠定了理论基础.
对简单类型理论进行扩展, 从而支持更丰富的类型, 可以使得Curry-Howard同构扩展到更丰富的逻辑, 如高阶逻辑, 能够表达更多有意义的定理.在Martin-Lof构造类型论(constructive type theory, 简称CTT)中[
对程序进行推理, 可以使用特定针对程序验证而开发的逻辑, 如Floyd-Hoare逻辑, 或者直接作用在编程语言的语义上.程序视为形式化的数学对象, 程序规范视为数学对象具有的性质, 因此, 程序验证可以理解成形式化的数学证明.下面我们来分析3种具有影响力的编程逻辑.
一阶编程逻辑, 也称为函数式语义(functional semantics), 是指将程序视为由输入状态映射到输出状态的递归函数, 因此, 程序性质可以使用递归归纳(recursion induction)进行验证.这种方法由McCarthy提出, 他也建立了一种新的递归函数理论, 即条件表达式(the theory of conditional expressions)理论来支持该方法[
McCarthy提出的这种方法将程序推理建立在递归函数上, 带有条件表达式的递归函数表达了程序语义.对程序性质进行推理时, 程序首先转化为递归函数, 递归函数的定义被翻译为逻辑等式.1976年, Cartwright和McCarthy展示了该逻辑能够用来推理递归函数的性质, 并适用于Pascal程序性质的推理[
归纳证明的机械化存在两个主要挑战:机器如何选择归纳变量以及如何找到有用的归纳公理[
理论上讲, 一阶编程逻辑更适合于如Lisp这类函数式编程语言, 因为这类编程语言避免了将程序转换成递归函数的麻烦.此外, 一阶编程逻辑的表达能力不及高阶逻辑, 也在一定程度上制约了这种逻辑系统的广泛应用.
Floyd-Hoare逻辑也称为归纳断言(inductive assertions).1967年, Floyd提出了证明程序正确性的基本思想[
Hoare公理系统吸引了众多学者对其展开后续研究, 这些研究包括循环不变式的构造、支持并发、指针等语言特性、终止性问题、该公理系统的可靠性和完备性问题等, 产生了很多研究成果.其中, 1975年, Dijstra提出了最弱前置条件(weakest precondition)和谓词转换器(predicate transformer)[
归纳断言系统除了需要自动定理证明工具之外, 验证条件生成器(verification condition generator, 简称VCG)是另一个重要的组成部分, 通过验证条件生成器将断言转换为验证条件, 即一阶公式, 然后再由自动定理证明工具进行证明.早期基于Floyd-Hoare逻辑的大型验证工具是Stanford Verifier和Gypsy Verification Environment(GVE)[
在归纳断言这种方法中, 程序以及加在程序上的注解被转换成大量逻辑公式, 当这些公式未通过证明时, 难以确定究竟是程序出了问题, 还是注解出了问题.而支持封装、继承、多态等面向对象特性编程语言的语义复杂性更加剧了这一问题的严重性.
旨在验证程序正确性的霍尔公理系统也被看成是一种公理语义(axiomatic semantics).公理语义没有操作语义中“状态”的概念, 程序变量的取值反映在断言中, 语义建立在这种断言上:断言是关于程序中变量取值的逻辑公式, 这些值随着程序的执行而发生改变, 但是存在着某种保持不变的关系, 程序执行前的初始断言和执行后的终止断言反映了这些不变式关系, 表示了这段程序代码的语义.从这种意义上讲, 公理语义是一种不直接的语义定义方式.
Milner于1968年实现了一个自动定理证明工具, 尽管他盛赞Robinson基于消解的证明技术, 但是他还是被这个工具所能证明出有意义定理的困难性所击败, Milner对机器辅助(machine-assisted)而不是完全自动的程序证明更感兴趣[
为了能够灵活地添加证明命令而不损害可靠性, 并可节约存储空间, Milner等人于1973年~1978年设计了Edinburg LCF[
为了方便证明命令的扩展和使用, Edinburg LCF设计了函数式编程语言ML(meta language), ML是严格类型化的, 用来支持抽象类型机制.分解待证明目标的证明命令如推理规则一样, 也实现为函数, 称为策略(tactics).策略是由目标(goal)到子目标(subgoal)的函数.策略能够以不同的方式组合成为新的策略, 组合方式也是一个ML函数, 称为tacticals.策略可以视为推理规则的逆, 支持了后向证明.可编程的Edinburgh LCF为用户提供了更多与机器的交互, 但并不损失可靠性.
Edinburgh LCF为证明助手的开发建立了一个标准框架, 许多后来的证明助手或多或少都采用了其中的核心技术特点.这些证明助手包括对Edinburgh LCF进行了大量改进和完善的Cambridge LCF[
Milner成功地将斯科特的域理论应用在实践中, 而域理论为Strachey.20世纪60年代所提出的指称语义(denotational semantics)奠定了数学基础[
由于指称语义的状态是程序状态, 即程序中各变量的取值, 它纯粹使用数学函数来定义状态的变化, 这使得LCF方法在推理程序的方式上非常不同于上述讨论的一阶编程逻辑和Floyd-Hoare逻辑.一阶编程逻辑和Floyd-Hoare逻辑都将程序语义嵌入在某种算法中:一阶编程逻辑将程序的语义转换为带有条件表达式的递归函数; Floyd-Hoare逻辑将程序语义通过验证条件生成器转换为验证条件; 而在LCF逻辑中, 程序是这个逻辑系统所操纵的对象, 因此程序的语义可以显式定义, 这也称为嵌入(embed)编程语言到证明助手中.事实上, 在Isabelle/HOL和Coq等证明助手中, 可以方便地定义大步操作语义和小步操作语义.程序的许多性质, 譬如程序的相等性、程序变换以及一致性和终止性等, 都能够方便地在证明助手的逻辑系统中得到表达.
从另外一方面来看, 由于Hoare逻辑是一种特定用于程序验证的逻辑, 证明程序的性质会更直接.为了充分利用LCF方法和Hoare逻辑的优势, Gordon、Mehta和Nipkow分别使用证明助手HOL和Isabelle/HOL, 将Hoare逻辑实现为推理出来的规则[
20世纪70年代, 定理证明工具的设计与实现围绕一阶逻辑而展开, 这在很大程度上是因为一阶逻辑具有很强的理论属性, 如完备性.然而, Gordon指出:这类属性对于验证是不相关的, 而简单类型理论, 即高阶逻辑所具有的额外表述力对于验证而言却是必要的[
当Paulson正在剑桥致力于Cambridge LCF的开发时, Gordon也正在剑桥从事着硬件验证的研究, 因此他对Cambridge LCF非常熟悉.Gordon对Milner所开发的通信演算系统(communication calculus system, 简称CCS)留有深刻印象, 他认识到:通过并行组合硬件系统中个体结构的描述, 可以计算推理得到整个硬件系统的行为.于是设计了称为LSM(logic of sequential machine)的符号, 用来表示机器的顺序行为, 并构造了一条类似CCS的Expansion Theorem的规则.接下来, Gordon对Cambridge LCF进行了改进, 使之适合LSM.这个改进的证明助手获得了初步成功, 对Viper处理器进行了规范和正确性证明[
高阶逻辑的选择在当时相当激进, 譬如高阶合一在理论上是不可判定的, 不过在实际中, Huet开发的半可判定的高阶合一算法[
程序构造(program construction)也称为程序综合(synthesis), 是指由规范(specification)构造出具体程序.一个主要方法是将由规范到实现的过程视为一系列对数据结构和控制结构进行求精(refinement)的程序变换, 因此, 程序构造也常和求精这一术语联系在一起.
逐步求精(step refinement)的程序构造技术最初由Dijstra[
旨在将逐步求精和程序变换与基于不变式的方法统一起来用于程序构造, 在一系列研究积累之上, Back利用Dijstra最弱前置条件演算, 于1988年提出了求精演算(refinement calculus)[
求精演算会产生大量既冗长又易错的谓词公式, 需要完成的工作非常艰巨.一些研究开始寻求机械化手段来支持求精演算[
求精的思想也由Abadi和Lamport用来证明分布式程序的低层规范正确实现了高层规范, 称为求精映射(refinement mapping)[
一个获得了工业级应用的逐步求精工具是B方法的工具包Atelier B[
基于定理证明方法的求精工具较为少见.就目前我们所知, Isabelle/HOL通过Locales机制支持逐步求精. Cornell大学的PRL团队维护着NuPRL的开发, 其中, PRL代表证明或程序求精逻辑(proof/program refinement logic).从技术发展上看, 求精的概念和应用非常宽泛, 譬如可以应用在编译器验证的研究中.
已经详细剖析了证明助手的主要理论基础和关键技术, 接下来讨论证明助手的实现和应用.限于篇幅, 仅针对部分主流证明助手的设计特点进行分析比较, 阐述具有代表性的证明助手的开发与实现.
证明助手的设计与实现并不像传统软件开发那样具有规范化的标准可以遵循, 特别是在早期阶段.从历史发展上看, 它的开发是一个从错误中不断修正、渐趋成熟的过程.不同证明助手之间相互影响, 一些完成了它的历史使命而终止开发或者进化成新的证明助手, 一些仍然活跃.在这个过程中, 逐步形成了开发一个现代证明助手所需要考虑的重要特点.本节先比较这些设计特点, 然后重点阐述几个具有代表性的证明助手的开发和实现.
针对证明助手的可靠性和使用性,
部分主流证明助手的特点比较
A comparison of features of some mainstream proof assistants
名称 | 小核 | 声明/过程式 | 实现语言 | 代码生成 | 用户界面 |
http://wiki.portal.chalmers.se/agda/pmwiki.php)]]> | √ | 声明式 | Haskell | 已可执行 | Emacs |
Coq | √ | 过程式 | OCaml | √ | IDE |
Nuprl | √ | 综合 | Common Lisp | √ | Emacs |
PVS | - | 过程式 | Common Lisp | √ | Emacs |
HOL4 | √ | 过程式 | Standard ML | √ | Emacs |
http://www.cl.cam.ac.uk/~jrh13/hol-light/)]]> | √ | 过程式 | OCaml | × | command- line based |
Isabelle | √ | Isar声明式 | Standard ML, Scala | √ | IDE |
ACL2 | — | 声明式 | Common Lisp | 已可执行 | Eclipse-based |
Mizar (mizar.uwb.edu.pl) | — | 声明式 | Free Pascal | — | Alcor |
各项特点分析如下.
(1) 小核
证明助手用来验证数学、计算机软/硬件的正确性, 它们本身是正确可靠的吗?一方面, 鉴于机器证明的机械刻板性, 即使存在某些缺陷, 它在证明定理时所具有的可靠性量级也远胜人工证明; 另一方面, 通常认为:如果一个证明助手具有相对较小的内核, 所有其他推理规则都是基于小核中的规则来定义的, 那么, 需要信任的就是这个小核[
在LCF方法的证明助手中, Agda、Coq、Nuprl和PVS是基于类型理论的, 它们通常会生成证明对象, 由一个相对简单的证明检查程序进行检查, 这个小程序可被认为是一个小核, 不过, PVS的设计者并不太关注理论上的可靠性, 而持有相当松散和实际的正确性观点, 本文中标记为“—”; LCF方法的直接后代:HOL4、HOL Light以及Isabelle本身就是基于非常小的可信内核来设计的.
ACL2在设计时注重强大的自动推理能力和使用上的方便; Mizar旨在建立形式化验证的数学知识库.因此, 对这两种证明助手不按小核标准进行比较, 显示为符号“—”.
(2) 声明/过程式证明语言
用户使用证明助手支持的证明语言与证明助手进行交互.证明语言可分为声明式和过程式两种:前者指出证明什么, 后者指明如何进行证明.因此, 声明式的证明可读性较高.
在早期基于LCF方法证明助手的开发中, 策略脚本是传统过程式的, 其晦涩难懂性与Mizar声明式证明语言的相对高可读性形成了巨大反差, 因此, Harrison倡导Mizar声明式证明语言[
(3) 实现语言
大多数证明助手, 譬如Coq、Isabelle等都是以函数式编程语言编写的, 譬如Haskell、Ocaml、Common Lisp、Standard ML以及Scala等.不过, Mizar的实现语言是Free Pascal, Free Pascal是Pascal编译器, 其目标平台包括多种处理器架构, 如Intel x86、AMD64/x86-64、PowerPC、MIPS和JVM等.
(4) 代码生成
许多证明助手支持代码生成, 或称为程序抽取(program extraction).代码生成是指将在证明助手中以证明语言书写的各种定义翻译成可执行的函数式程序, 可以独立运行.譬如, Isabelle/HOL可生成SML、OCaml和Haskell程序, Coq可以生成Ocaml、Haskell和Scheme程序, PVS可以生成Common Lisp程序, ACL2和Agda本身是可执行的.Mizar旨在建立合适的数学语言对数学进行形式定义和证明, 因此对它不考虑代码生成这个特点, 显示为符号“—”.
(5) 用户界面
证明助手建立在函数式编程语言之上, 使用命令行方式与之进行交互.Aspinall于1999年开发了Proof General[
一种不同的方法是通过证明助手集成开发环境框架(prover IDE framework, 简称PIDE)完成.PIDE非常类似于现代软件集成开发环境, 用户在输入源码时, IDE就检查语法.Coq和Isabelle现已支持这种用户界面, 分别称为GTK-based CoqIDE和the Isabelle/jEdit IDE[
以上分析比较了主流证明助手的设计特点, 为了更好地理解证明助手的设计,
一些证明助手的进化以及之间的相互影响
Evolvement of proof assistants and influences on each other
总体上讲, Milner设计的Edinburgh LCF和Bruijn设计的Automath[
Isabelle/HOL是当前被广泛使用的、LCF方法的证明助手, 它是建立在Isabelle元逻辑(meta-logic)之上的一个目标逻辑(object logic).Isabelle元逻辑也称为Isabelle/Pure.
Paulson于1985年开始Isabelle的开发, 他考虑以元逻辑, 即通用的、适用于多种特定逻辑的证明助手的开发.以Paulson的观点来看:许多特定逻辑证明助手开发的困难性都是类似的, 故开发通用证明助手可以一劳永逸地解决这些难题, 而将特定逻辑要解决的特定问题留给特定逻辑, 由以元逻辑为基础的目标逻辑去处理.
这种观点也体现在Edinburgh逻辑框架(logical framework, 简称LF)中[
在这些以逻辑框架为设计思想的证明助手中, Isabelle是唯一得到广泛应用的证明助手, 它可以视为LCF方法和逻辑框架的联合.
Isabelle元逻辑的实现基础是Church的简单类型理论, 是具有蕴含、全称量词和相等的高阶逻辑, 推理规则不是前提到结论的ML函数, 而是前提蕴含结论的公理, 允许目标逻辑以自然演绎风格进行构造.Isabelle/Pure并未利用类型化
受Huet的启发, Isabelle实现了高阶合一, 在高阶合一的基础上, Isabelle支持许多自动推理工具, 从而具有强大的自动推理功能:高阶重写的简化器Simplifier、结合了Metis证明工具的经典推理器(the classical reasoner)和经典Tableau证明工具; 支持使用外部自动定理证明工具, 如Vampire、SPASS的Sledghammer工具; 支持反例搜索的Quickcheck和Refute.此外, Isabelle使用Locales处理参数化的理论, 支持了模块化的理论开发(modular theory development).
由元逻辑Isabelle/Pure可以构造许多不同种类的目标逻辑(object logics), 譬如经典和直觉的一阶逻辑(Isabelle/FOL)、Martin-Lof构造类型理论(Isabelle/CTT)、一阶ZF集合论(Isabelle/ZF)以及经典的高阶逻辑Isabelle/HOL等, 如
Isabelle元逻辑和目标逻辑
Meta-logic and object logics of Isabelle
Isabelle/HOL是当前使用最多的一个目标逻辑, 在
图 8所示, 其中, HOL4、HOL Light、HOL Zero (http://proof-technologies.com/holzero/index.html)以及ProofPower(http://www.lemma-one.com/ProofPower/index/)现仍然在开发和维护中, 它们都是经典的高阶逻辑.HOL light由在Intel公司工作的Harrison于1994年推出.虽然始于硬件验证的动机, HOL系列也可以进行算法和程序验证, 并支持进程代数以及极限理论、微分和积分等经典数学验证.]]>
HOL系列的进化
Evolvement of HOL family
1984年, 法国国家信息与自动化研究所INRIA的Huet和Coquand决定实现构造演算(calculus of constructions, 简称CoC), 初始版本是一个证明检查器, 紧接着采纳了LCF方法的策略方式, 导致的系统可以视为Automath的Martin-Lof构造类型论的扩展, 综合了依赖类型和多态.之后, Mohring实现了称为Auto的证明搜索策略, 代表着Coq证明助手的诞生.Mohring和Coquand于1988年开始设计归纳构造演算(calculus of inductive constructions, 简称CIC).之后, Coq经历了反复的重设计和实现, 当前, Coq的稳定版本是8.8.0.一个新的扩展是Coq团队开始实现同伦类型理论.
http://metaprl.org).]]>
Coq与Nuprl都是使用了LCF方法且以类型理论而设计的证明助手.这类证明助手基于非简单的类型理论, 即依赖类型等.利用命题即类型、证明即项的思想, 类型化的
ACL2始于Boyer和Moore于1973年开发的纯粹Lisp定理证明工具, 该工具解决了归纳证明的机械化问题, 如第1.3.1节所述.之后, Boyer和Moore继续对其进行完善.20世纪80年代中期, Kaufmann加入了开发团队.经过多年的持续改进, Boyer和Moore终于实现了他们在1973年设计自动定理证明工具的目标:ACL2(a computational logic for applicative common Lisp)诞生[
PVS是Prototype Verification System的简称, 由SRI公司于1992年开始研发.PVS和ACL2一样具有强大的自动化证明能力, 但是PVS也意图提供如证明助手所具有的强表述力和逻辑, 提供了类Lisp语言供用户与之进行一定的交互.PVS是经典类型化的高阶逻辑, 但不像Coq和Nuprl那样产生独立可检查的证明对象.PVS当前的稳定版本是6.0.
从第一个定理证明工具至今, 经过约60多年的持续研究, 机械化定理证明在实际应用中产生了丰硕的研究成果, 以下从数学、编译器验证、操作系统微内核验证、电路设计验证等几个具有影响力的研究领域来讨论所取得的应用成果.
最早提出“数学机械化”思想, 并做出卓越贡献的是美籍华裔数理学家王浩先生.他于1959年编写了一个计算机程序, 实现了带有相等关系的谓词逻辑, 在很短时间内证明了Russell和Whitehead所著的数学原理中的几百条定理.秉承数学机械化的思想, 针对几何定理的机器证明, 吴文俊在1977年提出了“吴方法”:待证定理由坐标间的代数关系表示, 从而将平面几何问题代数化; 再通过多项式的消元法进行验证[
许多数学家们都接受了使用证明助手来证明数学定理.van BJLS使用Automath形式化了由Landau所著的数学教科书中的定理[
几个具有代表性的机器证明的数学定理列表
Lists of some representative mathematical theorems which are machined checked
证明时间(年) | 使用的证明助手 | 证明的数学定理 |
2005 | Isabelle/HOL | 质数定理(prime theorem) |
2009 | HOL light | 质数定理 |
2000~2005 | Coq | 四色定理(the four color theorem) |
2008 | Coq | 奇阶定理(Feit_Thompson) |
2014 | Isabelle/HOL, Coq, HOL Light | 开普勒猜想(Kepler conjecture) |
数学的机械化证明能够清除疑问, 解决模糊性, 并发现错误.正如Lakatos指出的:数学家们常会出错, 有时甚至连定义都会出错[
编译器是将高级语言编写的程序转换到能在目标平台上运行指令集的重要系统软件.当前, 绝大多数编译器都没有经过形式化验证, 虽然在发布前已经进行了大量测试, 但仍存在许多问题.形式化验证编译器的研究随着第一个高级语言编译器的诞生就开始展开.但是, 表达和证明编译器正确的困难性, 以及不断发展的高级编程语言带来的语义和编译转换过程的复杂性使得这项研究历经几十年而经久不衰.随着关键技术和证明助手的成熟, 编译器验证领域涌现出了大量研究成果.这些成果可以分为“验证的编译器(verified compiler)”和“验证编译器(verifying compiler)”[
传统的编译器自身正确性验证的方法原理源自莫里斯(Morris F. L.), 如
语义等同示意图
Semantics homomorphism diagram
伴随编程语言语义的不断发展进化,
编译器自身正确性的机器验证研究成果列表
Lists of achievements of verified compiler
起始年份 | 采用的证明助手 | 源语言 | 目标机器(语言) |
1972 | Stanford LCF | 类Algol | 简单机器汇编 |
1979 | Edinburgh LCF | SAL | 假想栈机 |
1981 | Stanford Verifier | 类Pascal | 类B6700栈机 |
1989 | Boyer-Moore | Micro-Gypsy | FM8502汇编 |
1991 | HOL | Vista汇编 | Viper处理器 |
1998 | PVS | Tosca | Aida |
1998 | Isabelle/HOL | Java子集 | Java虚拟机 |
2005 | Coq | C子集 | PowerPC汇编 |
1997 | OBJ3 | Occam子集 | Transputer机器 |
编译器的机器验证最开始针对的是实验性质的语言.20世纪80年代, 两个比较大型的编译器验证分别使用Stanford Verifier和Boyer-Moore定理证明工具完成.前者的源语言类似Pascal, 目标机器类似B6700, 源语言和目标机器指令的指称语义之间的等同性表示为断言(assertions)语言, 这些断言转换为验证条件, 再由Stanford Verifier进行证明[
到20世纪90年代, 更多的证明助手被开发出来.使用HOL, Curzon基于指称语义证明了一个结构化的汇编语言Vista到目标Viper微处理器的编译[
到20世纪末和21世纪初, 证明助手已渐趋成熟, 联合结构化操作语义和自然语义的出现, 这些为实际编程语言编译器的验证创造了良好条件.最具代表性的两个项目是使用Coq的C编译器CompCert, 以及使用Isabelle/HOL的Java编译器Jinja和JinjaThread, 下面分别予以阐述.
(1) C优化编译器CompCert
始于2005年, Leroy等人使用Coq定义了C语言子集(Clight)的大步操作语义, 经过多遍翻译变换, 完成了从Clight到PowerPC汇编码的验证, 如
CompCert多遍编译和中间语言
Compilation passes and intermediate languages of CompCert
严格上讲, 为了对优化算法进行验证, CompCert结合了编译后代码验证, 并辅以手工证明:编译器在编译转换的同时, 也生成安全性规范.对于编译器的每遍翻译, 证明翻译前后的语义等同; 或暂不证明而延迟到后续的某遍翻译中去验证翻译后的程序是否满足安全性规范, 并以注解的形式表示在翻译结果中; 最后对这些注解的一致性进行验证.国内王生原编译器研究组采用Coq实现了一个可信编译器L2C, L2C将同步数据流语言Lustre编译到了Clight, 他们对L2C的核心翻译步骤及其设计与实现进行了论述[
建立在CompCert2.0基础之上, Beringer等人证明了在共享内存交互情况下的编译优化[
(2) Java编译器Jinja和JinjaThread
Java编译器因其面向对象特性以及内建多线程机制而使得验证更为复杂.Nipkow和Oheimb首先于1998年使用Isabelle/HOL对Java子集进行了形式定义, 并证明了它的类型安全性[
Jinja语义等同框架(包括类型安全)的核心理论
Core theories of semantics homomorphism of Jinja (including type safety)
建立在Jinja基础之上, Lochbihler设计了一个能够定义线程的语义框架JinjaThread, 如
带有内存模型的JinjaThreads语义栈
Semantics stack of JinjaThreads with JMM
除了传统的语义等同原理方法外, 编译器自身验证的另外一种方法是采用如第1.5节所述的“构造即正确”的方法:定义程序转换规则, 源语言程序按照转换规则被逐步求精到可执行的目标语言程序.转换规则是编译器行为, 规则的可靠性保证编译的正确性.20世纪90年代初期开始的欧洲项目ProCos(provably correct systems)采用了类似方法[
在ProCos项目研究的大环境下, Sampaio使用项重写term rewriting系统OBJ3[
虽然从理论上讲, 这种编译器自身正确性验证方法的代数特性使得可以使用项重写工具对证明进行检查, 但是正如Sampaio所指出的:不能保证初始选择的一套代数法则的一致性.但是从Back和Wright的研究[
编译器自身的正确性验证需要准确定义源语言和目标语言的形式语义.形式语义的研究始于20世纪60年代, 操作语义、指称语义、公理语义以及代数语义构成了编程语言语义的四大主线, 陆汝钤深入剖析了这四大流派的形式语义以及形式语义学的现代应用[
鉴于编译器自身验证的困难性, 一些研究者转而对编译后的程序代码进行验证.一个具有影响力的成果是携带证明的代码(proof-carrying code, 简称PCC)[
认证编译器原理图
Framework of certifying compiler
这个出具证明的编译器只需要保证工具VCGen和Proof Checker的正确性, 无关复杂的编译器和证明助手.胡荣贵和陈意云等人通过构造扩展数据流图, 设计实现了从C语言子集源程序到携带类型注解的x86目标代码的认证编译器, 能够处理公共子表达式消除等优化操作[
另一个有影响力的成果是Pnueli等人提出了翻译确认(translation validation)[
翻译确认示意图
Framework of translation validation
Pnueli给出了同步语言Signal到目标C语言的翻译确认.虽然STS是非常通用的, 但是将正确实现定义为模拟求精可能更适合建立Signal同步语言到C之间的正确实现关系.翻译确认的思想是基于模拟的, 而不是严格意义上讲的证明构造的技术.与PCC相比, Pnueli提出的语法上的基于模拟的证明方法保证了验证的完全自动化, 而在PCC中, 正确性证明的关键部分是手工完成的; 此外, 翻译确认的基本思想以不同的实现和证明方式, 运用在了操作系统微内核seL4的源程序到ARM机器码的编译验证中, 接下来对此给出讨论.
2014年, 第一个验证的操作系统微内核seL4开源发布, 这是一个持续了约20年开发的研究成果.seL4作为L4操作系统验证家族的第三代, 致力于形式化验证可潜在应用于强调安全和关键性任务的操作系统内核程序, 提供了最基本也是最重要的操作系统服务:线程、进程间通信、虚拟内存、中断、授权机制等.整个系统可分为两部分:安全的操作系统内核源程序和该源程序到ARM机器码的翻译确认, 下面分别予以阐述.
(1) 安全的操作系统微内核源程序
工程上, 操作系统开发人员更倾向于从底层细节出发, 通过有效管理硬件而获得高性能, 而形式化方法的实践者更愿意采取一种自顶向下的开发方法, 始于硬件的高度抽象.seL4团队采取了一个折中方法:始于一个由函数式编程语言Haskell编写的可执行规范.sel4的设计过程如
seL4设计过程
sel4 design process
在这个设计中, 首先, 操作系统的需求由人工实现为可执行的Haskell代码, 称为Haskell原型(Haskell prototype).一方面, 该代码可以通过硬件模拟器导出为二进制码, 用于测试; 更为重要的是, 它能够自动导入到Isabelle/HOL中, 成为可执行规范(executable specification).抽象规范(abstract specification)定义了微内核系统各项操作的功能是什么, 并通过嵌入在Isabelle/HOL中的Hoare逻辑对其正确性进行陈述; 大多数定理都是有关不变式的:低层内存不变式、类型不变式、数据结构不变式、算法不变式等.抽象规范与可执行规范之间的求精证明建立了高层(抽象)与低层(具体)之间的对应关系:抽象规范中的所有Hoare逻辑属性对于可执行规范来讲也是成立的.Haskell原型、可执行规范以及抽象规范这3个部分之间的交互不断迭代, 最终达到会聚(convergence), 得到一个安全的Haskell微内核代码.
虽然Haskell原型是可执行的模型, 但是它并不满足高性能的需求.于是, seL4团队使用C编程语言手工重新实现了这个模型, 以允许更多优化, 而成为高性能的C实现(high performance C implementation).因此, 也必须建立高性能的C实现与可执行的规范之间的求精关系, 证明它不会产生比可执行规范更多的行为.
seL4团队于2009年完成了这个操作系统微内核源程序的正确性验证:没有死锁、活锁、空指针使用、缓冲区溢出、算术异常以及未初始化变量的使用, 因此获得了第一个高性能的安全操作系统微内核C源程序.
(2) 微内核源程序到ARM机器码的翻译确认
已经获得了安全的操作系统微内核高性能C源程序, 接下来待解决的问题是如何保证该源程序编译后的二进制代码的安全.seL4团队初始考虑使用在Coq中验证的C编译器CompCert进行编译, 但是效果不太理想: Coq对C语言标准的解释不同于Isabelle/HOL, 而调和这些不同并不容易——Coq的底层逻辑与Isabelle/HOL的底层逻辑不是直接兼容的.因此, seL4团队采用了Pnueli提出的翻译确认的基本思想:将源程序和目标程序转化成统一形式, 即描述控制流图的公共中间语言程序, 其简单的控制流机制和标准的算术操作为C语言、CPU指令集以及SMT的位向量理论(bit-vector theory)所共有, 这非常适合利用SMT求解器进行分析处理和证明检查.seL4的翻译确认原理如
seL4的翻译确认的正确性证明
Artifacts of correctness proof of the sel4 translation validation
在
安全可信的操作系统微内核seL4现在已经应用在了几个安全攸关的工业开发中, 譬如波音公司的无人驾驶小鸟直升机(little bird helicopter)项目.
国内的冯新宇等人在操作系统微内核验证方面也做出了比较有影响力的研究成果[
鉴于大规模集成电路的高额成本以及它们在许多安全攸关领域的应用, 硬件设计验证显得越来越重要.相比软件而言, 硬件设计的特性更益于进行自动验证, 在工业界也得到了许多成功应用.硬件验证传统上采用模拟技术, 不过, 学术界和工业界一直也在研究使用定理证明技术奠定更为可靠的硬件电路设计的正确性.
早期工业级验证由Moore和Lynch等人完成了AMD K5微处理器的浮点小数除法的正确性验证[
Gordon开创了使用高阶逻辑进行硬件设计验证的先河.Harrison和Kaivola使用HOL light对Intel处理器浮点小数算法进行了验证[
与高阶的交互式定理证明相比, 自动定理证明难以处理大型电路设计的验证问题, 这是由于大量变量和中间节点的提升, 计算呈指数倍增长而造成的.具有更高表述力的高阶逻辑能克服这些不足, 但是需要用户的介入, 该用户既应该是电路系统的设计专家, 又需要精通定理证明助手.这种困难性限制了高阶定理证明在工业界的使用, 工程师们宁愿选择更易于使用的工具; 通用理论库的建立应该有助于复杂的电路设计的验证, 在一定程度上能够减轻这种困难性.
机械化定理证明是历经60多年、稳步向前推进的研究领域.验证的C优化编译器CompCert以及操作系统微内核sel4在工业界的成功应用也充分说明这是一个有意义且可行的建构可信的软/硬件系统的方式.回到引言部分的问题, 这些成果究竟是如何取得的?
可以说, 这些成果的取得非常来之不易, 它们是无数哲学家、数学家、逻辑学家和计算机科学家智慧的结晶:20世纪上半叶对数学基础的严格辩论, 使得形式系统的表述能力和形式证明系统的推理能力得到了系统而深入的探索.20世纪下半叶, 机械化定理证明技术在计算机上优雅地实现了数理逻辑的严格推理, 并提供了人工完全不可比拟的检查证明的能力.尽管这条研究道路曲折而漫长, 但纵观整个过程, 它一直保持着生机和活力, 并最终成就斐然.机械化定理证明具有:
1) 高可靠性.它以数理逻辑和类型论的经典研究成果为基础, 由计算机自动或半自动地完成并检查证明, 这种机械性证明的可靠性远胜人类的手工证明;
2) 可执行性.除了提供可靠的证明结果, 大多证明助手都支持可执行性, 能够生成可执行代码获得原型工具, 通过运行测例, 确认(validate)所定义的形式规范的合法性;
3) 共享性.具有类似逻辑基础的不同证明助手之间能够共享证明结果, 如Isabelle/HOL和HOL 4以及HOL light之间等[
因此, 有理由乐观地估计, 机械化定理证明将不再只由少数人所掌握和推崇, 而将广泛成为数学研究、计算机软/硬件系统设计开发的一部分, 确保严格的正确性.一些重要问题和挑战包括:
(1) 并发程序的机械化证明.
并发程序的验证一直是具有挑战性的难题, 而机械化证明的研究成果更为少见.林惠民实现了世界上第一个通用交互式进程代数验证工具PAM[
致力于共享内存并发程序执行的安全问题, 许多研究围绕内存模型展开[
(2) 支持并发的面向对象语言的编译器验证.
虽然出现了一个验证的、支持面向对象特性和线程的Java编译器, 但是并没有考虑字节码到本地二进制码的正确翻译.此外, 并发以及可执行性都是需要进一步解决和完善的问题.
(3) 更加强大的证明助手的开发.
当前存在许多较为成熟的证明助手, 但是不尽完善, 仍然有待支持更强大的自动证明能力[
(4) 机械化定理证明的开发成本较高, 使用和掌握比较困难, 需要探讨解决方法.
本文在由何炎祥教授主持的与可信软件和可信编译等相关的项目执行过程中逐步形成.感谢何炎祥教授主持的博士讨论班上各位师生所发表的意见和建议.感谢各位审稿人和编辑提出的修改意见和建议.
Paulson LC. Computational logic:Its origins and applications. Proc. of the Royal Society A Mathematical Physical and Engineering Sciences, 2018, 474(2210):20170872.[doi:10.1098/rspa.2017.0872]
Wu WJ. Mathematics Mechanization. Beijing:Science Press, 2003(in Chinese).
吴文俊.数学机械化.北京:科学出版社, 2003.
Harrison J, Urban J, Wiedijk F. History of interactive theorem proving. Handbook of the History of Logic, 2014, 9(2):135-214.[doi:10.1016/B978-0-444-51624-4.50004-6]
Wang H. Toward mechanical mathematics. IBM Journal of Research and Development, 1960, 4:2-22.[doi:10.1147/rd.41.0002]
McCarthy J. Computer programs for checking mathematical proofs. In:Proc. of the 5th Symp. on Pure Mathematics of the American Mathematical Society. 1961. 219-227.[doi:10.2307/2270190]
Wos L, Pereira F, Hong R, Boyer RS, Moore JS, Bledsoe WW, Henschen LJ, Buchanan BG, Wrightson G, Green C. An overview of automated reasoning and related fields. Journal of Automated Reasoning, 1985, 1(1):5-48.[doi:10.1007/BF00244288]
Blazy S, Dargaye Z, Leroy X. Formal verification of a C compiler front-end. In:Proc. of the 14th Int'l Symp. on Formal Methods. Hamilton, 2006. 460-475.[doi:10.1007/11813040_31]
Leroy X. A formally verified compiler back-end. Journal of Automated Reasoning, 2009, 43(4):363-446.[doi:10.1007/s10817-009-9155-4]
Demange BD, Pichardie D. A formally verified SSA-based middle-end-Static single assignment meets CompCert. In:Proc. of the 21st European Conf. on Programming Languages and Systems. Tallinn, 2012. 47-66.
Klein G, Elphinstone K, Heiser G, Andronick J, Cock D, Derrin P, Elkaduwe D, Engelhardt K, Kolanski R, Norrish M, Sewell T, Tuch H, Winwood S. seL4:Formal verification of an OS kernel. In:Proc. of the 22nd Symp. on Operating Systems Principles. Montana, 2009. 207-220.
Sewell T, Myreen MO, Klein G. Translation validation for a verified OS kernel. ACM SIGPLAN Notices, 2013, 48(6):471-482.
Klein G, Andronick J, Elphinstone K, Murry T, Sewell T, Kolanski R, Heiser G. Comprehensive formal verification of an OS microkernel. ACM Trans. on Computer Systems, 2014, 32(1):136-156.
Nipkow T, Brinkop H. Amortized complexity verified. Journal of Automated Reasoning, 2018.
Eberl M, Haslbeck MW, Nipkow T. Verified analysis of random binary tree structures. In:Proc. of the ITP 2018. LNCS, 2018.
Bentkamp A, Blanchette JC, Klakow D. A formal proof of the expressiveness of deep learning. In:Proc. of the 8th Interactive Theorem Proving. Brasília, 2017. 46-64.
Song LH, Wang HT, Ji XJ, Zhang XY. Verification of file comparison algorithm fcomp in Isabelle/HOL. Ruan Jian Xue Bao/Journal of Software, 2017, 28(2):203-215(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5098.htm[doi:10.13328/j.cnki.jos.005098]
宋丽华, 王海涛, 季晓君, 张兴元.文件比较算法fcomp在Isabelle/HOL中的验证.软件学报, 2017, 28(2):203-215. http://www.jos.org.cn/1000-9825/5098.htm[doi:10.13328/j.cnki.jos.005098]
https://philpapers.org/rec/WADPAP]]>
Prawitz D. An improved proof procedure. Theoria, 1960, 26:102-139.
Davis M, Putnam H. A computing procedure for quantification theory. Journal of the ACM, 1960, 7:201-215.
Robinson JA. A machine-oriented logic based on the resolution principle. Journal of the ACM, 1965, 12(1):23-41.
Bibel W. Early history and perspectives of automated deduction. In:Proc. of the 30th German Conf. on Advances in Artificial Intelligence. Osnabrück, 2007. 2-18.
Fitting M. First-order Logic and Automated Theorem Proving. 2nd ed., Springer-Verlag, 1996.
Davis M, Logemann G, Loveland D. A machine procedure for theorem-proving. Communications of the ACM, 1962, 5(7):394-397.
Liu Y, Duan ZH, Tian C. NuTL2PFG:Checking satisfiability of νTL formulas. Ruan Jian Xue Bao/Journal of Software, 2017, 28(4):898-906(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5057.htm[doi:10.13328/j.cnki.jos.005057]
刘尧, 段振华, 田聪.NuTL2PFG:νTL公式的可满足性检查.软件学报, 2017, 28(4):898-906. http://www.jos.org.cn/1000-9825/5057.htm[doi:10.13328/j.cnki.jos.005057]
http://www.jstor.org/stable/20009142 [doi:10.2307/20009142]]]>
D'Agostino M. Classical natural deduction:We will show them! In:Proc. of the Essays in Honour of Dov Gabbay. 2005. 429-468.
Church A. A formulation of the simple theory of types. Journal of Symbolic Logic, 1940, 5(2):56-68.
Russell B, Whitehead A. Principia Mathematica, Vol.3. Cambridge: Cambridge University Press, 1994.
Kamareddine F, Laan T, Nederpelt R. A Modern Perspective on Type Theory. Springer-Verlag, 2005.
Andrews PB. An introduction to mathematical logic and type theory:To truth through proof. Applied Logic, 1986, 27(1):312-314.
Paulson LC. A Formulation of the Simple Theory of Types (for Isabelle). Berlin, Heidelberg:Springer-Verlag, 1990.
Awodey S, Pelayo Á, Warren MA. Voevodsky's univalence axiom in homotopy type theory. Notices of the American Mathematical Society, 2013, 60(8):1164-1167.
Prawitz D, Deduction N. A Proof-theoretical Study. Uppsala:Almqvist & Wilkselll, 1965.
Howard WA. The formulae-as-types notion of construction. In:Proc. of the H.b.Curry Essays on Combinatory Logic Lambda Calculus & Formalism. 1980. 480-490(Originally appeared in 1969).
Martin-Lof P. Intuitionistic type theory. In:Proc. of the Notes by Giovanni Sambin of a Series of Lecturees Give in Padua. Bibliopolis, 1980.
Coquand T, Huet G. The calculus of constructions. Information and Computation, 1988, 76(2):95-120.
Bertot Y, Casteran P. Interactive Theorem Proving and Program Development:Coq'Art:The Calculus of Inductive Constructions. Berlin:Springer-Verlag, 2010.
McCarthy J. Towards a mathematical theory of computation. In:Proc. of the Western Joint IRE-AIEE-ACM Computer Conf. New York, 1961. 225-328.
https://www.researchgate.net/publication/244996781_A_PRACTICAL_FORMAL_SEMANTIC_DE_NITION_AND_VERI_CATION_SYSTEM_FOR_TYPED_LISP]]>
Carwright R, McCarthy J. First order programming logic. In:Proc. of the 6th ACM Sigact-Sigplan Symp. on Principles of Programming Languages. New York, 1979. 68-80.
Bledsoe WW. Splitting and reduction heuristics in automatic theorem proving. Artificial Intelligence, 1971, 2:55-77.
Boyer RS, Moore JS. Proving theorems about LISP functions. Journal of the ACM, 1973, 22(1):486-493.
Moore JS, Wirth CP. Automation of mathematical induction as part of the history of logic. Computer Science, arXiv:1309.6226, 2013.
Walther C. Mathematical Induction:Handbook of Logic in Artificial Intelligence and Logic Programming. Oxford:Oxford University Press, 1994.
Floyd RW. Assigning meanings to programs. In:Proc. of the American Mathematical Society Symp. on Applied Mathematics. 1967, 19:19-31.
Hoare CAR. An axiomatic basis for computer programming. Communications of the ACM, 1969, 12:576-580.
Edsger W. Dijkstra, guarded commands, nondeterminancy and formal derivation of program. Communications of the ACM, 1975, 18(8):453-457.
Igarashi S, London R, Luckham DC. Automatic program verification Ⅰ: A logical basis and its implementation. Technical Report, ISI/RR-73-11, Information Science Institute, 1973.
Good D, Cohen Richard M, Lawrence HW. A report on the development of Gypsy. In:Proc. of the 1978 Annual Conf. ACM Press, 1978. 116-122.[doi:10.1145/800127.804078]
Filliâtre JC, Marché C. The why/krakatoa/caduceus platform for deductive program verification. In:Proc. of the 19th Int'l Conf. on Computer Aided Verification. Berlin, 2007. 173-177.
Barnett M, Deline R, Jacobs B, Fähndrich M, Leino MRK, Schulte W, Venter H. The Spec# programming system:Challenges and directions. In:Proc. of the Verified Software:Theories, Tools, Experiments. Berlin, Heidelberg:Springer-Verlag, 2008. 144-152.
Flanagan C, Leino KRM, Lillibridge M, Nelson KRM, Saxe JB, Stata R. Extended static checking for Java. Technical Report, 159, Compaq Systems Research Center, 1998.
Barnes J. High Integrity Software:The SPARK Approach to Safety and Security. Addison Wesley, 2003.
Gordon AD, Harper R, Harrison J, Jeffrey A, Sewell P. Robin milner 1934~2010:Verification, languages, and concurrency. In:Proc. of the 43th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. Pittersburg, 2016. 473-474.
Scott DS. A type-theoretical alternative to ISWIM, CUCH, OWHY. Theoretical Computer Science, 1993, 121(1-2):411-440.
Milner R. Implementation and applications of Scott's logic for computable functions. In:Proc. of the Conf. on Proving Assertions About Programs. ACM Press, 1972. 1-6.
Gordon MJ, Milner AJ, Wadsworth P. A mechanised logic of computation. In:LNCS 78. 1979.
Paulson LC. Logic and Computation:Interactive Proof with Cambridge LCF. Cambridge University Press, 1987.
Gordon MJ, Melham TF. Introduction to HOL:A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993.
Constable RL, Allen SF, Bromley HM, Cleaveland WR, Cremer JF, Harper RW, Howe DJ, Knoblock TB, Mendler NP, Panangaden P, Sasaki J T, Smith SF. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 1987.
Scott DS. Towards a mathematical semantics for computer language. In:Proc. of the Symp. on Computers and Automation. 1971. 19-46.
Plotkin G. A structural approach to operational semantics. Journal of Logic & Algebraic Programming, 1981, s 60-61:17-139.
Despeyroux J. Proof of translation in natural semantics. In:Proc. of the 1st Symp. on Logic in Computer Science. 1986. 16-18.
Gordon MJC. Mechanizing programming logics in higher order logic. In:Current Trends in Hardware Verification and Automated Theorem Proving. 1989. 387-439.
Mehta F, Nipkow T. Proving pointer programs in higher-order logic. Information and Computation, 2005, 199(1-2):200-227.
Gordon MJ. Why higher-order logic is a good formalism for specifying and verifying hardware. In:Proc. of the Edinburgh Workshop Formal Aspects of VLSI Design. Amsterdam, 1986. 153-177.
Wagner TJ. Hardware verification[Ph.D. Thesis]. Stanford University, 1977.
Cohn A. A proof of correctness of the Viper microprocessor:The first level. In:Proc. of the VLSI Specification, Verification and Synthesis. Springer US, 1988. 27-71.
Huet GP. A unification algorithm for typed λ-calculus. Theoretical Computer Science, 1975, 1(1):27-57.
Paulson LC. Isabelle:The next 700 theorem provers. Computer Science, 2000, 310(1):772-773.
Gordon M. From LCF to HOL:A short history. In:Proc. of the Proof, Language, and Interaction, Essays in Honour of Robin Milner. DBLP, 2000. 169-186.
Dijkstra EW. A constructive approach to the problem of program correctness. BIT Numerical Mathematics, 1968, 8(3):174-186.
Wirth N. Program development by stepwise refinement. Commmunications of ACM, 1971, 14(4):221-227.
Gerhart SL. Correctness-preserving program transformations. In:Proc. of the 2nd Symp. on Principles of Programming Languages. California, 1975. 54-66.[doi:10.1145/512976.512983]
Burstall RM, Darlington J. A transformation system for developing recursive programs. ACM SIGPLAN Notices, 1975, 10(6):465-472.
Manna Z, Waldinger R. A deductive approach to program synthesis. Readings in Artificial Intelligence & Software Engineering, 1980, 2(1):90-121.
Back RJR. A calculus of refinements for program derivations. Acta Informatica, 1988, 25(6):593-624.
Li B, Tang ZH, Zhai J, Zhao JH. Verification of concrete programs with respect to abstract programs. Ruan Jian Xue Bao/Journal of Software, 2017, 28(4):786-803(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5195.htm[doi:10.13328/j.cnki.jos.005195]
李彬, 汤震浩, 翟娟, 赵建华.通过抽象程序证明复杂具体程序.软件学报, 2017, 28(4):786-803. http://www.jos.org.cn/1000-9825/5195.htm[doi:10.13328/j.cnki.jos.005195]
Vickers T. An overview of a refinement editor. In:Proc. of the Institution of Radio and Electronic Engineers. 1990.
Groves L, Nickson R, Utting M. A tactic driven refinement tool. In:Proc. of the 5th Refinement Workshop. London, 1992. 272-297.
Back RJ, von Wright J. Refinement concepts formalized in higher order logic. Formal Aspects of Computing, 1990, 2(1):247-272.
Wright JV. Program refinement by theorem prover. In:Proc. of the 6th Refinement Workshop. London:Springer-Verlag, 1994. 121-150.
Abadi M, Lamport L. The existence of refinement mapppings. Theorectical Computer Science, 1991, 82(2):253-384.
Lamport L. The Temporal Logic of Actions. ACM Press, 1994.
Jonsson B. Simulations between specifications of distributed systems. In:Proc. of the 2nd Int'l Conf. on Concurrency Theory. Amsterdam, 1991. 346-360.
Lynch NA, Vaandrager FW. Forward and backward simulations for timing-based Systems. In:Proc. of the Real-Time:Theory in Practice, REX Workshop. Berlin, Heidelberg:Springer-Verlag, 1991. 391-446.
Pnueli A, Rosner R. On the synthesis of a reactive module. In:Proc. of the 16th Symp. on Principles on Programming Languages. Texas, 1989. 179-190.
Abrial JR. The B-book:Assigning Programs to Meanings. Cambridge University Press, 1996.
Clearsy. ATELIER B Interactive Prover Reference Manual. 2016.
Geuvers H. Proof assistants history, ideas and future. Sadhana, 2009, 24(1):3-25.
Harrison J. A Mizar mode for HOL. In:Proc. of the 9th Int'l Conf. on Theorem Proving in Higher-Order Logics. Turku, 1996. 203-220.
Wenzel M. Isar:A generic interpretative approach to readable formal proof documents. In:Proc. of the Int'l Conf. on Theorem Proving in Higher Order Logics. Berlin, Heidelberg:Springer-Verlag, 1999. 167-183.
Gonthier G, Mahboubi A, Tassi E. A small scale reflection extension for the Coq system. Research Report, RR-6455, INRIA, 2008.
Wiedijk F. A synthesis of the procedural and declarative styles of interactive theorem proving. Logical Methods in Computer Science, 2012, 8(1):106-108.
Aspinall D. Proof general:A generic tool for proof development. In:Proc. of the 6th Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, 2000. 38-43.
Bertot Y, Théry L. A generic approach to building user interfaces for theorem provers. Journal of Symbolic Computation, 1998, 25(2):161-194.
Wenzel M. Isabelle/jEdit-A prover IDE within the PIDE framework. Computer Science, 2012. 468-471.
Cairns P. Alcor:A user interface for Mizar. Mechanized Mathematics & Its Applications, 2008, 4(1):2005.
De Bruijn NG. AUTOMATH:A language for mathematics. In:Automation of Reasoning. 1968. 159-200.
Harper R, Honsell F, Plotkin G. A framework for defining logics. In:Proc. of the 8th Symp. on Logic in Computer Science. Montreal, 1993. 143-184.
Nipkow T, Wenzel M, Paulson LC. Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer-Verlag, 2002(latest available in 2014).
Wenzel M. Shared-memory multiprocessing for interactive theorem proving. In:Proc. of the 4th Interactive Theorem Proving. Rennes, 2013. 418-434.
Wenzel M. Parallel proof checking in Isabelle/Isar. In:Proc. of the ACM SIGSAM Workshop on Programming Languages for Mechanized Mathematics Systems. 2009.
Kaufmann M, Manolios P, Moore JS. Computer-aided Reasoning:ACL2 Case Studies. Kluwer Academic Publishers, 2000.
Rager DL, Jr WAH, Kaufmann M. A parallelized theorem prover for a logic with parallel execution. In:Proc. of the 4th Int'l Conf. on Interactive Theorem Proving. Rennes, 2013. 435-450.
Wu WT. On the decision problem and the mechanization of theorem-proving elementary geometry. Science in China, 1979, 6:94-102.[doi:10.1142/9789812791085_0008]
Yang L, Zhang JZ, Hou XR. The Series in Nonlinear Science:Nonlinear Algebraic Equations and Theorem Proving. Shanghai:Shanghai Education Press, 1996(in Chinese).
杨路, 张景中, 侯晓荣.非线性科学丛书:非线性代数方程组与定理机器证明.上海:上海科技教育出版社, 1996.
Yang L, Xia BC. Inequality Proving and Automatic Discovery. Beijing:Science Press, 2008(in Chinese).
杨路, 夏壁灿.数学机械化丛书:不等式机器证明与自动发现.北京:科学出版社, 2008.
van Benthem Jutting LS. Checking Landau's "Grundlagen" in the automath system. Studies in Logic and the Foundations of Mathematics, 1994, 133:701-720.
Trybulec A. The Mizar-QC/6000 logic information language. ALLC Bulletin, 1978, 6(2).
Hurd J. Verification of the Miller-Rabin probabilistic primality test. Journal of Logic & Algebraic Programming, 2001, 56(1):3-21.
Hölzl J. Markov chains and Markov decision processes in Isabelle/HOL. Journal of Automated Reasoning, 2017, 59:345-387.
Nipkow T, Bauer G, Schultz P. 2006 Flyspeck Ⅰ:Tame graphs. In:Proc. of the 3rd Int'l Joint Conf. Seattle, 2006. 21-35.
Hales T, Adams M, Bauer G, Dang DT, Harrison J, Le Hoang T, Kaliszyk C, Magron V, McLaughlin S, Nguyen TT, Nguyen TQ, Nipkow T, Obua S, Pleso J, Rute J, Solovyev A, Ta AHT, Tran TN, Trieu DT, Urban J, Vu KK, Zumkeller R. A formal proof of the Kepler conjecture. Forum of Mathematics, 2017, 5.
Appel K, Haken W. Every planar map is four colorable. Bulletin of the American Mathematical Society, 1976, 82:711-712.
Gonthier G. The four color theorem:Engineering of a formal proof. In:Proc. of the Computer Mathematics. Springer-Verlag, 2008. 333.
Lakatos I, Worrall J, Zahar E. Proofs and refutations:The logic of mathematical discovery. Mathematical Gazette, 2015, 61(416):xii, 174-146.
Avigad J, Harrison J. Formally verified mathematics. Communications of the ACM, 2014, 57(4):66-75.
https://www.cl.cam.ac.uk/~lp15/Grants/Alexandria/]]>
Ma S, Shi ZP, Shao ZZ, Guan Y, Li L, Li Y. Higher-order logic formalization of conformal geometric algebra and its application in verifying a robotic manipulation algorithm. Advances in Applied Clifford Algebras, 2016, 26(4):1305-1330.[doi:10.1007/s00006-016-0650-5]
Ma S, Shi ZP, Li LM, Guan Y, Zhang J, Song XY. Formalization of geometric algebra theories in higherorder logic. Ruan Jian Xue Bao/Journal of Software, 2016, 27(3):497-516(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/4977.htm[doi:10.13328/j.cnki.jos.004977]
马莎, 施智平, 李黎明, 关永, 张杰, Xiao-Yu SONG.几何代数的高阶逻辑形式化.软件学报, 2016, 27(3):497-516. http://www.jos.org.cn/1000-9825/4977.htm[doi:10.13328/j.cnki.jos.004977]
Safonov VO. Trustworthy Compilers. John Wiley & Sons, 2010.
He YX, Wu W. Theories and Technologies of Trusted Compiler Construction. Beijing:Science Press, 2013(in Chinese).
何炎祥, 吴伟.可信编译构造理论与关键技术.北京:科学出版社, 2013.
Morris FL. Advice on structuring compilers and proving them correct. In:Proc. of the 1st Symp. on Principles of Programming Languages. Massachusetts, 1973. 144-152.
Polak W. Compiler Specification and Verification. Springer-Verlag, 1981.
Young WD. Verified compilation in micro-Gypsy. In:Proc. of the 3rd Symp. on Software Testing, Analysis, and Verification. Florida, 1989. 20-26.[doi:10.1145/75308.75312]
Moore JS. A mechanically verified language implementation. Journal of Automated Reasoning, 1989, 5(4):461-492.
Curzon P. A verified compiler for a structured assembly language. In:Proc. of the Int'l Workshop on the HOL Theorem Proving System and its Applications. 1991. 253-262.
Stringer-Calvert DWJ. Mechanical verification of compiler correctness[Ph.D. Thesis]. York University, 1998.
Liu Y, Gan YK, Wang SY, Dong Y, Yang F, Shi G, Yan X. Trustworthy translation for eliminating high-order operation of a synchronous dataflow language. Ruan Jian Xue Bao/Journal of Software, 2015, 26(2):332-347(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/4785.htm[doi:10.13328/j.cnki.jos.004785]
刘洋, 甘元科, 王生原, 董渊, 杨斐, 石刚, 闫鑫.同步数据流语言高阶运算消去的可信翻译.软件学报, 2015(2):332-347. http://www.jos.org.cn/1000-9825/4785.htm[doi:10.13328/j.cnki.jos.004785]
CDATA[Shang S, Gan YK, Shi G, Wang SY, Dong Y. Key translations of the trustworthy compiler L2C and its design and implementation. Ruan Jian Xue Bao/Journal of Software, 2017, 28(5):1233-1246(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5213.htm[doi:10.13328/j.cnki.jos.005213]
尚书, 甘元科, 石刚, 王生原, 董渊.可信编译器L2C的核心翻译步骤及其设计与实现.软件学报, 2017, 28(5):1233-1246. http://www.jos.org.cn/1000-9825/5213.htm[doi:10.13328/j.cnki.jos.005213]
Beringer L, Stewart G, Dockins R, Appel WA. Verified compilation for shared-memory C. In:Proc. of the 23rd European Symp. on Programming Languages and Systems. Grenoble, 2014. 107-127.
Sevcik J, Vafeiadis V, Nardelli FZ, Jagannathan S, Sewell P. Relaxed-memory concurrency and verified compilation. ACM SIGPLAN Notices, 2011, 46(1):43-54.
Nipkow T, Oheimb DV. Java light is type-safe definitely. In:Proc. of the 3rd Symp. on Principles on Programming Languages. California, 1998. 161-170.
Klein G. Verified bytecode verifiers[Ph.D. Thesis]. Technical University of Munich, 2002.
Klein G, Nipkow T. A machine-checked model for Java-like language, virtual machine and compiler. In:Proc. of the 33rd European Symp. on Programming Languages and Systems. South Carolina, 2006. 619-695.
Lochbihler A. A machine-checked, type-safe model of Java concurrency:Language, virtual machine, memory model, and verified compiler[Ph.D. Thesis]. Karlsruher Institute Technology, 2012.
Lochbihler A. Making the Java memory model safe. ACM Trans. on Programming Languages & Systems, 2014, 35(4):1-65.
He YX, Jiang N, Li QA, Zhang J, Shen FF. Machine-checked model for Micro-Dalvik virtual machine. Ruan Jian Xue Bao/Journal of Software, 2015, 26(2):364-379(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/4787.htm[doi:10.13328/j.cnki.jos.004787]
何炎祥, 江南, 李清安, 张军, 沈凡凡.一个机器检测的Micro-Dalvik虚拟机模型.软件学报, 2015, 26(2):364-379. http://www.jos.org.cn/1000-9825/4787.htm[doi:10.13328/j.cnki.jos.004787]
Jiang N, He YX, Zhang XT. mJava compiler targeting Micro-Dalvik virtual machine. Acta Electronica Sinica, 2016, 44(7):1619-1629(in Chinese with English abstract).
江南, 何炎祥, 张晓瞳.mJava到Micro-Dalvik虚拟机的编译验证.电子学报, 2016, 44(7):1619-1629.
Mike H, Bowen Jonathan P, Ernst-Rudiger O. Provably Correct Systems. Springer Publishing Company, 2017.
He J, Hoare CAR, Fränzle M, Muller-Olm M. Provably correct systems. LNCS, 1994, 863:288-335.[doi:10.1007/3-540-58468-4_171]
Buth B, Buth KH, Fränzle M, Karger B, Lakhneche Y, Langmaack H, Muller-Olm M. Provably correct compiler development and implementation. In:Proc. of the Int'l Conf. on Compiler Construction. 1992. 141-155.
He J, Page I, Bowen JP. A provably correct hardware implementation of Occam. ESPRIT ProCoS project document[OU HJF 9/5], Oxford University Computing Laboratory, 1992.
Zhou CC, Hoare CAR, Ravn AP. A calculus of durations. Information Processing Letters, 1991, 40(5):269-276.[doi:10.1016/0020-0190(91) 90122-X]
Hansen MR, Zhou C. Duration calculus:Logical foundations. Formal Aspects of Computing, 1997, 9(3):283-330.[doi:10.1007/BF01211086]
Zhou CC, Hansen MR, Sestoft P. Decidability and undecidability results for duration calculus. In:Proc. of the 10th Symp. on Theoretical Aspects of Computer Science. Würzburg:Springer-Verlag, 1993. 58-68.
Goguen J, Winklerz T, Meseguerz J, Futatsugix K, Jouannaud JP. Introducing OBJ. Technical Report, SRI Int'l, 1993.
Sampaio A. An algebraic approach to compiler design[Ph.D. Thesis]. Oxford University, 1993.
Morris JM. Laws of data refinement. Acta Informatica, 1989, 26:287-308.
Hoare CAR, He J, Sampaio A. Normal form approach to compiler design. Acta Informatica, 1993, 30(8):701-739.
Duran A, Cavalcanti A, Sampaio A. An Algebraic Approach to the Design of Compilers for Object-Oriented Languages. SpringerVerlag, 2010.
Lu RQ. Formal Semantics of Computing Systems. Beijing:Tsinghua University Press, 2017(in Chinese).
陆汝钤.计算系统的形式语义(上下).北京:清华大学出版社, 2017.
Necula GC. Proof-carrying code. In:Proc. of the 2nd Symp. on Principles on Programming Languages. San Francisco, 1997. 106-119.
Hu RG, Chen YY, Guo F, Zhang Y. Design and implementation of a certifying compiler for type-based annotation. Journal of Computer Research and Development, 2004, 41(1):28-33(in Chinese with English abstract).
胡荣贵, 陈意云, 郭帆, 张昱.基于类型注解的认证编译器设计与实现.计算机研究与发展, 2004, 41(1):28-33.
Pnueli A, Siegel M, Singerman E. Translation validation. In:Proc. of the 4th Tools and Algorithms for Construction and Analysis of Systems. Lisbon, 1998. 151-166.
Xu FW, Fu M, Feng XY, Zhang X, Zhang H, Li Z. A practical verification framework for preemptive OS kernels. In: Proc. of the Computer Aided Verification. Springer Int'l Publishing, 2016.
Moore JS, Lynch T, Kaufmann M. A mechanically checked proof of the correctness of the kernel of the AMD5K86 floating point division algorithm. IEEE Trans. on Computers, 1996, 47:913-926.
Russinoff DM. A mechanically checked proof of IEEE compliance of the floating point multiplication, division and square root algorithms of the AMD-K7TM processor. Journal of Computation & Mathematics, 1998, 1:148-200.
Sammane GA, Schmaltz J, Toma D, Ostier P, Borrione D. TheoSim:Combining symbolic simulation and theorem proving for hardware verification. In:Proc. of the 17th Symp. on Integrated Circuits and System Design. Pernambuco, 2004. 60-65.[doi:10.1145/1016568.1016591]
Hunt WA. Verifying VIA NANO microprocessor components. In:Proc. of the 10th Formal Methods in Computer-Aided Design. Lugano, 2010. 3-10.
Sawada J, Sandon P, Paruthi V, Baumgartner J. Hybrid verification of a hardware modular reduction engine. In:Proc. of the 11th Int'l Conf. on Formal Methods in Computer-Aided Design. Texas, 2011. 207-214.
Harrison J. Floating point verification in HOL light:The exponential function. In:Proc. of the 3rd Int'l Conf. on Algebraic Methodology and Software Technology. Sydney, 1997. 246-260.
Kaivola R, Kohatsu K. Proof engineering in the large:Formal verification of Pentium®4 floating-point divider. Int'l Journal on Software Tools for Technology Transfer, 2003, 4(3):323-334.
Harrison J. Formal verification at Intel. In:Proc. of the Logic in Computer Science. Ottawa, 2003. 45-54.
O'Leary J, Zhao X, Gerth R, Seger CJ. Formally verifying IEEE compliance of floating-point hardware. Intel Technical Journal. 1999. 69-72.
Tverdyshev S. A verified platform for a gate-level electronic control unit. In:Proc. of the 9th Formal Methods in Computer-Aided Design. Austin, 2009. 164-171.
Deng H. Formal verification of FPGA based systems[MS. Thesis]. Department of Conmputer and Sofrware, McMaster University, 2011.
Berg C, Jacobi C. Formal Verification of the VAMP Floating Point Unit. Berlin, Heidelberg:Springer-Verlag, 2001.
Braibant T. Coquet: A Coq library for verifying hardware. In: Proc. of the 1st Certified Programs and Proofs, Vol. 7086. Kenting: Springer-Verlag, 2011. 330-345.
Shiraz S, Hasan O. A HOL library for hardware verification using theorem proving. IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems, 2018,PP(99):1. [doi: 10.1109/TCAD.2017.2705049]
Mclaughlin S. An interpretation of Isabelle/HOL in HOL light. In:Proc. of the 3rd Int'l Joint Conf. on Automated Reasoning. Springer-Verlag, 2006. 192-204.
Lin H. PAM:A process algebra manipulator. Formal Methods in System Design, 1995, 7(3):243-259.
Lin H. A verification tool for value-passing process algebras. In:Proc. of the IFIP TransactionsC-16:Protocol Specification, Testing and Verification. 1993. 79-92.
Jiang YY, Xu C, Ma XX, Lü J. Approaches to obtaining shared memory dependences for dynamic analysis of concurrent programs:A survey. Ruan Jian Xue Bao/Journal of Software, 2017, 28(4):747-763(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5193.htm[doi:10.13328/j.cnki.jos.005193]
蒋炎岩, 许畅, 马晓星, 吕建.获取访存依赖:并发程序动态分析基础技术综述.软件学报, 2017, 28(4):747-763. http://www.jos.org.cn/1000-9825/5193.htm[doi:10.13328/j.cnki.jos.005193]
Aspinall D, Ševčík J. Formalising Java's Data Race Free Guarantee. Berlin, Heidelberg:Springer-Verlag, 2007. 22-37.
Batty M, Owens S, Sarkar S, Sewell P, Weber T. Mathematizing C++ concurrency. In: Proc. of the 38th Symp. on Principles on Programming Languages. Austin, 2011.
Ševčík J. Safe optimisations for shared-memory concurrent programs. In: Proc. of the 32nd Conf. on Programming Language Design and Implementation. San Jose, 2011.
Pichon-Pharabod J, Sewell P. A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions. In:Proc. of the 43rd Symp. on Principles on Programming Languages. St. Petersburg, 2016. 622-633.
Liang H, Feng X, Fu M. Rely-guarantee-based simulation for compositional verification of concurrent program transformations. ACM Trans. on Programming Languages & Systems, 2014, 36(1):1-55.
Liang H, Feng X. A program logic for concurrent objects under fair scheduling. In:Proc. of the 43rd Symp. on Principles on Programming Languages. St. Petersburg, 2016. 385-399.
Zhang HR, Fu M. Design and implementation of Coq tactics based on Z3. Ruan Jian Xue Bao/Journal of Software, 2017, 28(4):819-826(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5196.htm[doi:10.13328/j.cnki.jos.005196]
张恒若, 付明.基于Z3的Coq自动证明策略的设计和实现.软件学报, 2017, 28(4):819-826. http://www.jos.org.cn/1000-9825/5196.htm[doi:10.13328/j.cnki.jos.005196]
Alemi AA, Chollet F, Een N, Irving G, Szegedy C, Urban J. DeepMath-Deep sequence models for premise selection. In: Proc. of the NIPS 2016. 2016.
Loos S, Irving G, Szegedy C, Kaliszyk C. Deep network guided proof search. In: Gauthier T, Kaliszyk C, Urban J, eds. Proc. of the TacticToe: Learning to Reason with HOL4 Tactics (LPAR 2017). 2017.