The Verified Incremental Design of a Distributed Spanning Tree Algorithm: Extended Abstract

The paper announces an incremental mechanically–verified design of the algorithm of Gallager, Humblet, and Spira for the distributed determination of the minimum-weight spanning tree in a graph of processes. The processes communicate by means of asynchronous messages with their neighbours in the graph. Messages over one link may pass each other. The proof of the algorithm is based on ghost variables, invariants, and a decreasing variant function. The verification is mechanized by means of the theorem prover Nqthm of Boyer and Moore. This extended abstract is an introduction to the full paper that can be obtained by ftp (http://link.springer.de/link/service/journals/00165/). Received May 1997 / Accepted in revised form January 1995     

Using an induction prover for verifying arithmetic circuits

We show that existing theorem proving technology can be used effectively for mechanically verifying a family of arithmetic circuits. A theorem prover implementing: (i) a decision procedure for quantifier-free Presburger arithmetic with uninterpreted function symbols; (ii) conditional rewriting; and (iii) heuristics for carefully selecting induction schemes from terminating recursive function definitions; and (iv) well integrated with backtracking, can automatically verify number-theoretic properties of parameterized and generic adders, multipliers and division circuits. This is illustrated using our theorem prover Rewrite Rule Laboratory (RRL). To our knowledge, this is the first such demonstration of the capabilities of a theorem prover mechanizing induction. The above features of RRL are briefly discussed using illustrations from the verification of adder, multiplier and division circuits. Extensions to the prover likely to make it even more effective for hardware verification are discussed. Furthermore, it is believed that these results are scalable, and the proposed approach is likely to be effective for other arithmetic circuits as well.     

Frame rule for mutually recursive procedures manipulating pointers

Using a predicate transformer semantics of programs, we introduce statements for heap operations and separation logic operators for specifying programs that manipulate pointers. We prove a powerful Hoare total correctness rule for mutually recursive procedures manipulating pointers. The rule combines earlier proof rules for (mutually) recursive procedures with the frame rule for pointer programs. The theory, including the proofs, is implemented in the theorem prover PVS. In this implementation program variables and addresses can store values of almost any type of the theorem prover.     

Apla中泛型约束机制研究

泛型程序设计可大幅提高程序的可重用性、可靠性和开发效率.泛型约束机制是对泛型参数进行形式描述,并对其合法性进行检测及验证,从而保证泛型程序的可靠性和安全性.分析总结多种主流语言的泛型约束特性,存在难以描述及验证基于动态语义的复杂约束需求问题,与完整实现GP尚有距离;以抽象程序设计语言Apla为宿主语言,提出了基于代数结构及公理语义的泛型约束方法,给出了基本数据类型、自定义抽象数据类型和子程序的3类泛型约束机制,拓展了泛型程序设计约束的应用范围.同时,支持静态语法和动态语义层约束,提高了泛型约束的精确度;借助Isabelle定理证明器,设计了泛型约束匹配检测和验证算法;进一步设计了泛型约束机制在PAR平台的实现方案及其系统原型.实验部分给出了该泛型约束机制描述、检测及验证一系列复杂泛型约束问题的全过程,自动生成的C++模板程序的可靠性和安全性得到显著提高.     

Automatic inductive theorem proving using prolog

Although Prolog is a programming language based on techniques from theorem proving, its use as a base for a theorem prover has not been explored until recently (Stickel, 1984). In this paper, we introduce a Prolog-based deductive theorem proving method for proving theorems in a first-order inductive theory representable in Horn clauses. The method has the following characteristics:

• 1.It automatically partitions the domains over which the variables range into subdomains according to the manner in which the predicate symbols in the theorem are defined.
• 2.For each of the subdomains the prover returns a lemma. If the lemma is true, then the target theorem is true for this subdomain. The lemma could also be an induction hypothesis for the theorem.
• 3.The method does not explicitly use any inductive inference rule. The induction hypothesis, if needed for a certain subdomain, will sometimes be generated from a (limited) forward chaining mechanism in the prover and not from employing any particular inference rule.

In addition to the backward chaining and backtracking facilities of Prolog, our method introduces three new mechanism—skolemization by need, suspended evaluation, and limited forward chaining. These new mechanisms are simple enough to be easily implemented or even incorporated into Prolog. We describe how the theorem prover can be used to prove properties of Prolog programs by showing two simple examples.     

Poitín: Distilling Theorems From Conjectures

In this paper, we describe a new fully automatic theorem prover called Poitín which makes use of a novel transformation algorithm called distillation to prove input conjectures. The input conjectures are defined in a functional language and are transformed using the distillation algorithm. The result of this transformation can be easily inspected to see whether the original conjecture is true. Possible divergence of the transformation algorithm is detected, and this information is used to perform generalizations to ensure termination. We give several examples of the application of the theorem prover, and compare it to related work.     

Interaction with the Boyer-Moore theorem prover: A tutorial study using the arithmetic-geometric mean theorem

There are many papers describing problems solved using the Boyer-Moore theorem prover, as well as papers describing new tools and functionalities added to it. Unfortunately, so far there has been no tutorial paper describing typical interactions that a user has with this system when trying to solve a nontrivial problem, including a discussion of issues that arise in these situations. In this paper we aim to fill this gap by illustrating how we have proved an interesting theorem with the Boyer-Moore theorem prover: a formalization of the assertion that the arithmetic mean of a sequence of natural numbers is greater than or equal to their geometric mean. We hope that this report will be of value not only for (non-expert) users of this system, who can learn some approaches (and tricks) to use when proving theorems with it, but also for implementors of automated deduction systems. Perhaps our main point is that, at least in the case of Nqthm, the user can interact with the system without knowing much about how it works inside. This perspective suggests the development of theorem provers that allow interaction that is user oriented and not system developer oriented. This research was supported in part by ONR Contract N00014-94-C-0193. The views and conclusions contained in this document are those of the author(s) and should not be interpreted as representing the official policies, either expressed or implied, of Computational Logic, Inc., the Office of Naval Research, or the U.S. government.     

Locales: A Module System for Mathematical Theories

Locales are a module system for managing theory hierarchies in a theorem prover through theory interpretation. They are available for the theorem prover Isabelle. In this paper, their semantics is defined in terms of local theories and morphisms. Locales aim at providing flexible means of extension and reuse. Theory modules (which are called locales) may be extended by definitions and theorems. Interpretation to Isabelle’s global theories and proof contexts is possible via morphisms. Even the locale hierarchy may be changed if declared relations between locales do not adequately reflect logical relations, which are implied by the locales’ specifications. By discussing their design and relating it to more commonly known structuring mechanisms of programming languages and provers, locales are made accessible to a wider audience beyond the users of Isabelle. The discussed mechanisms include ML-style functors, type classes and mixins (the latter are found in modern object-oriented languages).     

Mechanical reasoning about families of UTP theories

The Unifying Theories of Programming (UTP) of Hoare and He is a general framework in which the semantics of a variety of specification and programming languages can be uniformly defined. In this paper we present a semantic embedding of the UTP into the ProofPower-Z theorem prover; it concisely captures the notion of UTP theory, theory instantiation, and, additionally, type restrictions on the alphabet of UTP predicates. We show how the encoding can be used to reason about UTP theories and their predicates, including models of particular specifications and programs. We support encoding and reasoning about combinations of predicates of various theory instantiations, as typically found in UTP models. Our results go beyond what has already been discussed in the literature in that we support encoding of both theories and programs (or their specifications), and high-level proof tactics. We also create structuring mechanisms that support the incremental construction and reuse of encoded theories, associated laws and proof tactics.     

A theorem prover for verifying iterative programs over integers

An implementation of a rule-based theorem prover for verifying iterative programs over integers is presented. The authors emphasize the overall proof construction strategy of the prover which has been able to construct the correctness proofs of all iterative programs taken from the literature. Two performance measures for the prover are proposed, and its proof construction for an array-sorting program is evaluated using these measures     

Formalizing provable anonymity in Isabelle/HOL

We formalize in a theorem prover the notion of provable anonymity. Our formalization relies on inductive definitions of message distinguishing ability and observational equivalence on traces observed by the intruder. Our theory differs from its original proposal and essentially boils down to the inductive definition of distinguishing messages with respect to a knowledge set for the intruder. We build our theory in Isabelle/HOL to achieve a mechanical framework for the analysis of anonymity protocols. Its feasibility is illustrated through two case studies of the Crowds and Onion Routing protocols.     

Specification and Verification of Concurrent Programs Through Refinements

We present a framework for the specification and verification of reactive concurrent programs using general-purpose mechanical theorem proving. We define specifications for concurrent programs by formalizing a notion of refinements analogous to stuttering trace containment. The formalization supports the definition of intuitive specifications of the intended behavior of a program. We present a collection of proof rules that can be effectively orchestrated by a theorem prover to reason about complex programs using refinements. The proof rules systematically reduce the correctness proof for a concurrent program to the definition and proof of an invariant. We include automated support for discharging this invariant proof with a predicate abstraction tool that leverages the existing theorems proven about the components of the concurrent programs. The framework is integrated with the ACL2 theorem prover and we demonstrate its use in the verification of several concurrent programs in ACL2.     

基于子空间信息量准则的前向神经网络设计理论与方法研究

从理论上提出了子空间信息量(SIQ)及其准则(SIQC)的概念；在此基础上阐述了基于上述准则的前向神经网络设计的相关理论，包括前向神经网络隐含层信息量(HLIQ)、存在性和逼近定理，给出了选择隐含层神经元数、权值向量集和隐含层激励函数的指导方向；提出了基于上述理论的一种可行的次优网络设计算法；最后，详细分析了网络性能指标及其影响因素，上述理论和方法完全克服了传统学习算法的各种弊端，丰富了前向神经网络设计领域的理论依据，具有较大的理论指导和实际应用价值，文中通过具体实例验证了上述理论和方法的可行性和优越性．     

Formalizing non-interference for a simple bytecode language in Coq

In this paper, we describe the application of the interactive theorem prover Coq to the security analysis of bytecode as used in Java. We provide a generic specification and proof of non-interference for bytecode languages using the Coq module system. We illustrate the use of this formalization by applying it to a small subset of Java bytecode. The emphasis of the paper is on modularity of a language formalization and its analysis in a machine proof. C. B. Jones     

Possible events, actual events, and robots

To plan means reasoning about possible actions, but a robot must also reason about actual events. This paper proposes a formal theory about actual and possible events. It presents a new modal logic as a notation for this theory and a technique for planning in the modal logic using a first-order theorem prover augmented with simple modal reasoning. This avoids the need for a general modal-logic theorem prover. Adding beliefs to this theory raises an interesting problem for which the paper offers a tentative solution.     

Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs

We describe a combination of BDDs and superposition theorem proving, called light-weight theorem proving, and its application to the flexible and efficient automation of the reasoning activity required to debug and verify pointer manipulating programs. This class of programs is notoriously challenging to reason about and it is also interesting from a programming point of view since pointers are an important source of bugs. The implementation of our technique (in a system called haRVey) scales up significantly better than state-of-the-art tools such as E (a superposition prover) and Simplify (a prover based on the Nelson and Oppen combination schema of decision procedures which is used in ESC/Java) on a set of proof obligations arising in debugging and verifying C functions manipulating pointers.     

The Warshall Algorithm and Dickson's Lemma: Two Examples of Realistic Program Extraction

By means of two well-known examples it is demonstrated that the method of extracting programs from proofs is manageable in practice and may yield efficient programs. The Warshall algorithm computing the transitive closure of a relation is extracted from a constructive proof that repetitions in a path can always be avoided. Second, we extract a program from a classical (i.e., nonconstructive) proof of a special case of Dickson's lemma, by transforming the classical proof into a constructive one. These techniques (as well as the examples) are implemented in the interactive theorem prover MINLOG developed at the University of Munich.     

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.     

基于涟波下降规则的设计知识管理系统

自动化服务组合技术是程序生成方法在Semantic Web Services领域的一种应用.该文提取了服务的"输入"、"输出"、"前置条件"、"执行效果"、"执行功能",定义了服务的语义5元组.通过一个转换模版,把服务描述表述成一阶谓词逻辑公式,根据"证明与程序等价"的理论,利用自动化定理证明系统,完成从已有服务到目标服务的逻辑证明,从所记录的证明路径中提取目标服务的实现体,介绍了实现这一技术的原型系统.