针对教学场景的ZFC集合论Coq形式化

离散数学是计算机类专业的基础课程之一,命题逻辑、一阶逻辑与公理集合论是其重要组成部分.教学实践表明,初学者准确理解语法、语义、推理系统等抽象概念是有一定难度的.近年来,已有一些学者开始在教学中引入交互式定理证明工具,以帮助学生构造形式化证明,更透彻地理解逻辑系统.然而,现有的定理证明器有较高上手门槛,直接使用会增加学生的学习负担.鉴于此,在Coq中开发了针对教学场景的ZFC公理集合论证明器.首先,形式化了一阶逻辑推理系统和ZFC公理集合论;之后,开发了数条自动化推理规则证明策略.学生可以在与教科书风格相同的简洁证明环境中使用自动化证明策略完成定理的形式化证明.该工具被用在了大一新生离散数学课程的教学中,没有定理证明经验的学生使用该工具可以快速完成数学归纳法和皮亚诺算术系统等定理的形式化证明,验证了该工具的实际效果.     

一个命题投影时序逻辑符号模型检测器

现有模型检测工具的形式化规范语言,如计算树逻辑(computation tree logic,简称CTL)和线性时序逻辑(linear temporal logic,简称LTL)等的描述能力不足,无法验证ω正则性质.提出了一个命题投影时序逻辑(propositional projection temporal logic,简称PPTL)符号模型检测工具——PLSMC(PPTL symbolic model checker)的设计与实现过程.该工具基于著名的符号模型检测系统NuSMV,实现了PPTL的符号模型检测算法.PLSMC的规范语言PPTL具有完全正则表达能力,这使得定性性质和定量性质均可被验证.此外,PLSMC可以有效地缓解模型检测工具中容易发生的状态空间爆炸问题.最后,利用PLSMC对铁路公路交叉道口护栏控制系统的安全性质和周期性性质进行验证.实验结果表明,PPTL符号模型检测工具扩充了NuSMV系统的验证能力,使得时间敏感、并发性和周期性等实时性质可以被描述和验证.     

区间时序逻辑的标记相继式演算

区间逻辑在许多领域如人工智能,形式化方法中都有成功应用。其中,区间时序逻辑及其各种扩充近年来越来越多地受到人们的重视,由于区间时序逻辑具有较强的表达能力,这也使得该逻辑的定理证明变得相当困难,该文提出了区间时序逻辑的一个标记相继式演算,并给出其可靠性和相对完备性结论。该演算应用于机器辅助定理证明工具中,可以有效地提高证明的自动化程度,在高阶逻辑证明了工具ＰＶＳ中,作者尝试性地实现了这一演算,获得了     

有穷时间投影时序逻辑的完备公理系统

为采用定理证明的方法对并发及交互式系统进行验证,研究了有穷论域下有穷时间一阶投影时序逻辑(projection temporal logic,简称PTL)的一个完备公理系统.在介绍PTL的语法、语义并给出公理系统后,提出了PTL公式的正则形(normal form,简称NF)和正则图(normal form graph,简称NFG).基于NF给出了NFG的构造算法,并利用NFG可描述公式模型的性质证明PTL公式的可满足性判定定理和公理系统的完备性.最后,结合实例展示了PTL及其公理系统在系统验证中的应用.结果表明,基于PTL的定理证明方法可方便用于并发系统的建模与验证.     

行为时序逻辑与自反线性时序逻辑的关系

为了能够将哲学逻辑中的公理系统运用到行为时序逻辑的研究中。对行为时序逻辑公式的语义进行形式化定义．从语义和语法两方面研究行为时序逻辑公理系统和具有自反性质的线性时序逻辑公理系统之间的联系．提出并证明行为时序逻辑公式转换为自反线性时序逻辑公式的定理。按照集合论和模型论的思想,定义行为时序逻辑中项和行为时序逻辑原子公式的概念。定义Lesilie Lamport所提出的行为时序逻辑公式的语义。证明自反线性时序逻辑公理系统适用于行为时序逻辑公理系统．以此为基础证明行为时序逻辑的简单规则、基本规则和附加规则。     

步进索引模型下的语义及其形式化

霍尔逻辑作为计算机程序的逻辑基础,可以用于描述一般程序的验证.分离逻辑作为霍尔逻辑的扩展,可以支持很多现代程序语言中的高阶特性.步进索引模型被用于定义自递归谓词.步进索引逻辑被广泛应用于各种基于交互式定理证明器的程序验证工具中,然而,基于步进索引逻辑的推理却比经典逻辑复杂、繁琐.事实上,也可以在步进索引模型上定义更加简洁清晰的、与“步数”无关的经典逻辑体系下的非步进索引程序语义.人们希望找到步进索引逻辑和非步进索引逻辑之间的关系,但发现两种逻辑并不等价.对实际的程序验证工作中涉及的命题进行归纳总结,找出它们共同的特征,给出关于程序状态的断言的约束条件;分别定义步进索引逻辑和非步进索引逻辑体系中断言的语义,并证明在该约束条件下两种语义的等价性;在Coq中,形式化以上所有定义和证明;最后,对未来值得关注的研究方向进行初步探讨.     

GJK算法的一种特殊情形的形式化验证和应用

计算几何算法经常用于机器人避碰运动规划等安全攸关领域,对这些算法进行正确性证明非常重要.用形式化方法对算法进行验证是一种十分有效的手段,尤其是定理证明的方法用严格的数学公理和定理推理证明逻辑模型的性质,对所验证的性质而言是完备的.基于GJK算法设计了计算空间两条线段间距离的算法,用定理证明器HOL4对其相关的定义和定理进行形式化定义和证明,进而基于霍尔逻辑完成形式化表示和证明,对该算法的正确性实现了形式化验证.最后,给出了这一经过验证的算法在双臂机器人无碰撞运动规划中的应用.     

出具证明编译器中线性整数命题证明的自动生成

近年来,出具证明编译器作为构建高可信软件的重要途径,逐渐成为编译器理论和形式化验证的研究热点.在其理论框架中,编译器需要借助自动定理证明技术,自动地证明验证条件并生成机器可检查的证明项,因此好的自动定理证明器对出具证明编译器至关重要.本文基于Simplex算法在出具证明编译器的框架内设计并实现了一个支持线性整数命题求解的自动定理证明器,并且提出一套证明项构造方法,将其应用于自动定理证明器中可生成Coq可检查的证明.     

基于交互式定理证明的并发程序验证工作综述

并发程序与并发系统可以拥有非常高的执行效率和相对串行系统较快的响应速度,在现实中有着非常广泛的应用。但是并发程序与并发系统往往难以保证其实现的正确性,实际应用程序运行中的错误会带来严重的后果。同时,并发程序执行时的不确定性会给其正确性验证带来巨大的困难。在形式化验证方法中,人们可以通过交互式定理证明器严格地对并发程序进行验证。本文对在交互式定理证明中可用于描述并发程序正确性的验证目标进行总结,它们包括霍尔三元组、可线性化、上下文精化和逻辑原子性。交互式定理证明方法中常用程序逻辑对程序进行验证,本文分析了基于并发分离逻辑、依赖保证逻辑、关系霍尔逻辑等理论研究的系列成果与相应形式化方案,并对使用了这些方法的程序验证工具和程序验证成果进行了总结。     

基于事件确定有限自动机的UML2.0 序列图描述与验证

为了确保软件分析与设计阶段UML2.0序列图模型的可靠性,采用命题投影时序逻辑(propositional projection temporal logic,简称PPTL)模型检测方法对该模型进行分析和验证.提出了事件确定有限自动机(event deterministic finite automata,简称ETDFA),并使用该自动机为序列图建立形式化模型,通过给出的基于ETDFA的PPTL模型检测算法得到验证结果.该方法可以在基于Spin的PPTL模型检测器的支持下实现.实例结果表明,该方法可以验证序列图的性质并保证其可靠性.     

Proving linearizability with temporal logic

Linearizability is a global correctness criterion for concurrent systems. One technique to prove linearizability is applying a composition theorem which reduces the proof of a property of the overall system to sufficient rely-guarantee conditions for single processes. In this paper, we describe how the temporal logic framework implemented in the KIV interactive theorem prover can be used to model concurrent systems and to prove such a composition theorem. Finally, we show how this generic theorem can be instantiated to prove linearizability of two classic lock-free implementations: a Treiber-like stack and a slightly improved version of Michael and Scott’s queue.     

Coq Formalization of ZFC Set Theory for Teaching Scenarios

Discrete mathematics is a foundation course for computer-related majors, and propositional logic, first-order logic, and the axiomatic set theory are important parts of this course. Teaching practice shows that beginners find it difficult to accurately understand abstract concepts, such as syntax, semantics, and reasoning system. In recent years, some scholars have begun introducing interactive theorem provers into teaching to help students construct formal proofs so that they can understand logic systems more thoroughly. However, directly employing the existing theorem provers will increase students'' learning burden since these tools have a high threshold for getting started with them. To address this problem, we develop a prover for the Zermelo-Fraenkel set theory with the axiom of Choice (ZFC) in Coq for teaching scenarios. Specifically, the first-order logical reasoning system and the axiomatic set theory ZFC are formalized, and several automated proof tactics specific to reasoning rules are then developed. Students can utilize these automated proof tactics to construct formal proofs of theorems in a textbook-style concise proving environment. This tool has been introduced into the teaching of the course of discrete mathematics for freshmen. Students with no prior theorem-proving experience can quickly construct formal proofs of theorems including mathematical induction and Peano arithmetic with this tool, which verifies the practical effectiveness of this tool.     

First-Order Temporal Verification in Practice

First-order temporal logic, the extension of first-order logic with operators dealing with time, is a powerful and expressive formalism with many potential applications. This expressive logic can be viewed as a framework in which to investigate problems specified in other logics. The monodic fragment of first-order temporal logic is a useful fragment that possesses good computational properties such as completeness and sometimes even decidability. Temporal logics of knowledge are useful for dealing with situations where the knowledge of agents in a system is involved. In this paper we present a translation from temporal logics of knowledge into the monodic fragment of first-order temporal logic. We can then use a theorem prover for monodic first-order temporal logic to prove properties of the translated formulas. This allows problems specified in temporal logics of knowledge to be verified automatically without needing a specialized theorem prover for temporal logics of knowledge. We present the translation, its correctness, and examples of its use. Partially supported by EPSRC project: Analysis and Mechanisation of Decidable First-Order Temporal Logics (GR/R45376/01).     

Translation Templates to Support Strategy Development in PVS

In presenting specifications and specification properties to a theorem prover, there is a tension between convenience for the user and convenience for the theorem prover. A choice of specification formulation that is most natural to a user may not be the ideal formulation for reasoning about that specification in a theorem prover. However, when the theorem prover is being integrated into a system development framework, a desirable goal of the integration is to make use of the theorem prover as easy as possible for the user. In such a context, it is possible to have the best of both worlds: specifications that are natural for a system developer to write in the language of the development framework, and representations of these specifications that are well matched to the reasoning techniques provided in the prover. In a tactic-based prover, these reasoning techniques include the use of tactics (or strategies) that can rely on certain structural elements in the theorem prover's representation of specifications. This paper illustrates how translation techniques used in integrating PVS into the TIOA (Timed Input/Output Automata) system development framework produce PVS specifications structured to support development of PVS strategies that implement reasoning steps appropriate for proving TIOA specification properties.     

The Watson Theorem Prover

Watson is a general-purpose system for formal reasoning. It is an interactive equational higher-order theorem prover. The higher-order logic supported by the prover is distinctive in being type free (it is a safe variant of Quine's NF). Watson allows the development of automated proof strategies, which are represented and stored by the prover in the same way as theorems. The mathematical foundations of the prover and the way these are presented to a user are discussed. The paper also contains discussions of experiences with the prover and relations of the prover to other systems.     

Weakest pre-condition reasoning for Java programs with JML annotations

This paper distinguishes several different approaches to organising a weakest pre-condition (WP) calculus in a theorem prover. The implementation of two of these approaches for Java within the LOOP project is described. This involves the WP-infrastructures in the higher order logic of the theorem prover PVS, together with associated rules and strategies for automatically proving JML specifications for Java implementations. The soundness of all WP-rules has been proven on the basis of the underlying Java semantics. These WP-calculi are integrated with the existing Hoare logic, and together form a verification toolkit in PVS: typically one uses Hoare logic rules to break a large verification task up into smaller parts that can be handled automatically by one of the WP-strategies.     

实时系统的形式化验证

实时系统的设计对系统设计人员而言是一个巨大挑战。在缺乏严格的验证环境时 ,要避免设计错误是很困难的。本文将一种带时戳的时序逻辑及用于描述具体实时系统的时间变迁系统编码到 HOL定理证明器中 ,并实现了一个基本的规则策略库 ,从而实现了一个简单的交互式辅助验证环境L RP。实例 Fisher算法的互斥性在 IRP中得到了验证。     

Muse—A Computer Assisted Verification System

Muse is a verification system which extends the collection of tools developed by SRI International for their Hierarchical Development Methodology (HDM). It enhances the SRI system by providing a capability for proving invariants and constraints for the state machine described by a specification written in SPECIAL (the specification language of HDM). In particular, it enables one to use the HDM system to meet the requirements for formal verification in a National Computer Security Center A1 evaluation of a secure operating system. In addition to the tools provided by SRI, Muse has a parser, a facility to handle multiple modules, a formula generator, and a theorem prover. The theorem prover has a number of interesting features designed to facilitate human direction of the proving process. In concept, it is open-ended. We introduce the notion of a theorem prover kernel as a device for ensuring the logical soundness of the prover in the face of continual improvements to its functionality.     

Formal verification of concurrent programs using the Larch prover

The paper describes the use of the Larch prover to verify concurrent programs. The chosen specification environment is UNITY, whose proposed model can be fruitfully applied to a wide variety of problems and modified or extended for special purposes. Moreover, UNITY provides a high level of abstraction to express solutions to parallel programming problems. We investigate how the UNITY methodology can be mechanized within a general purpose first order logic theorem prover like LP, and how we can use the theorem proving methodology to prove safety and liveness properties. Then we describe the formalization and the verification of a communication protocol over faulty channels, using the Larch prover LP. We present the full computer checked proof, and we show that a theorem prover can be used to detect flaws in a system specification