Verifying a logic-synthesis algorithm and implementation: a casestudy in software verification

We describe the verification of a logic synthesis tool with the Nuprl proof development system. The logic synthesis tool, Pbs, implements the weak division algorithm. Pbs consists of approximately 1000 lines of code implemented in a functional subset of Standard ML. It is a proven and usable implementation and is an integral part of the Bedroc high level synthesis system. The program was verified by embedding the subset of Standard ML in Nuprl and then verifying the correctness of the implementation of Pbs in the Nuprl logic. The proof required approximately 500 theorems. In the process of verifying Pbs we developed a consistent approach for using a proof development system to reason about functional programs. The approach hides implementation details and uses higher order theorems to structure proofs and aid in abstract reasoning. Our approach is quite general, should be applicable to any higher order proof system, and can aid in the future verification of large software implementations     

Efficient multiple-precision integer division algorithm

Design and implementation of division algorithm is one of the most complicated problems in multi-precision arithmetic. Huang et al. [1] proposed an efficient multi-precision integer division algorithm, and experimentally showed that it is about three times faster than the most popular algorithms proposed by Knuth [2] and Smith [3]. This paper reports a bug in the algorithm of Huang et al. [1], and suggests the necessary corrections. The theoretical correctness proof of the proposed algorithm is also given. The resulting algorithm remains as fast as that of [1].     

二维不规则图形和即制板电路区域运算的算法研究

区域运算是轮廓求解算法集中的核心算法．本文介绍适用于复杂ＰＣＢ电路和二维不规则图案的一种区域运算算法，阐述了它的数学模型、算法描述、正确性证明和复杂性分析．与典型的算法比较，它有明显的优越性．     

Generalization in the presence of free variables: A mechanically-checked correctness proof for one algorithm

We present a case study in which an automated proof assistant was used to show the correctness of an algorithm. Specifically, we document the application of an extension of the Boyer-Moore Theorem Prover to the problem of verifying the correctness of an implementation of generalization, where the proof had surprisingly many details and a previous implementation contained an error. We attempt to provide sufficient detail so that the reader can gain a realistic impression of the nature of this exercise.This research was supported in part by ONR Contrast N00014-88-C-0454. The views and conclusions contained in this document are those of the author 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.     

Correctness of constructing optimal alphabetic trees revisited

Several new observations which lead to new correctness proofs of two known algorithms (Hu-Tucker and Garsia-Wachs) for construction of optimal alphabetic trees are presented. A generalized version of the Garsia-Wachs algorithm is given. Proof of this generalized version works in a structured and illustrative way and clarifies the usually poorly understood behavior of both the Hu-Tucker and Garsia-Wachs algorithms. The generalized version permits any nonnegative weights, as opposed to strictly positive weights required in the original Garsia-Wachs algorithm. New local structural properties of optimal alphabetic trees are given. The concept of well-shaped segment (a part of an optimal tree) is introduced. It is shown that some parts of the optimal tree are known in advance to be well-shaped, and this implies correctness of the algorithms rather easily. The crucial part of the correctness proof of the Garsia-Wachs algorithm, namely the structural theorem, is identified. The correctness proof of the Hu-Tucker algorithm consists of showing a very simple mutual simulation between this algorithm and the Garsia-Wachs algorithm. For this proof, it is essential to use the generalized version of Garsia-Wachs algorithm, in which an arbitrary locally minimal pair is processed, not necessarily the rightmost minimal pair. Such a generalized version is also needed for parallel implementations. Another result presented in this paper is the clarification of the problem of resolving ties (equalities between weights of items) in the Hu-Tucker algorithm. This is related to the proof, by simulation, of correctness of the Hu-Tucker algorithm. It is shown that the condition that there are no ties may generally be assumed without harm and that, essentially, the Hu-Tucker algorithm avoids ties automatically.     

基于语法树和程序正确性验证研究

提出了一种新的基于语法树的程序正确性验证方法(TM方法)在理论和算法上对方法的实现进行了初步探讨,并结合XML技术提出了一套实现这一方法的切实可行的解决方案.     

Formal Verification of an Executable LTL Model Checker with Partial Order Reduction

We present a formally verified and executable on-the-fly LTL model checker that uses ample set partial order reduction. The verification is done using the proof assistant Isabelle/HOL and covers everything from the abstract correctness proof down to the generated SML code. Building on Doron Peled’s paper “Combining Partial Order Reductions with On-the-Fly Model-Checking”, we formally prove abstract correctness of ample set partial order reduction. This theorem is independent of the actual reduction algorithm. We then verify a reduction algorithm for a simple but expressive fragment of Promela. We use static partial order reduction, which allows separating the partial order reduction and the model checking algorithms regarding both the correctness proof and the implementation. Thus, the Cava model checker that we verified in previous work can be used as a back end with only minimal changes. Finally, we generate executable SML code using a stepwise refinement approach. We test our model checker on some examples, observing the effectiveness of the partial order reduction algorithm.     

Studies of a Theory of Specifications with Built-in Program Extraction

We present a Theory of Specifications based on Martin-Löf's type theory, with rules for simultaneously constructing programs and their correctness proofs. The theory contains types for representing specifications whose corresponding notion of implementation is that of a pair formed by a program and a correctness proof. The rules of the theory are such that in implementations the program parts appear mixed together with the proof parts. A confluent and normalizing computational relation performs the task of separating programs from proofs. As a consequence, every implementation computes to a pair composed of a program and a proof of its correctness, and so the program extraction procedure is immediate.     

一种极小化覆盖的空间索引结构——MCSI-树

以缩小各层节点覆盖为目标,运用数据空间分割技术,结合二叉树和R-树思想,提出一种空间数据索引结构——MCSI-树。在该结构中,空间数据之间的拓扑关系得到记载,各层节点的覆盖明显减少,查询区域减小,使区域查询速度得到提高。给出MCSI-树的建立算法及算法的正确性、可终止性证明及时间复杂度,并给出节点插入算法。     

A Certifying Code Generation Phase

Guaranteeing correctness of compilation is a vital precondition for correct software. Code generation can be one of the most error-prone tasks in a compiler. One way to achieve trusted compilation is certifying compilation. A certifying compiler generates for each run a proof that it has performed the compilation run correctly. The proof is checked in a separate theorem prover. If the theorem prover is content with the proof one can be sure that the compiler produced correct code. This paper reports on the construction of a certifying code generation phase for a compiler. It is part of a larger project aimed at guaranteeing the correctness of a complete compiler. We emphasize on demonstrating the feasibility of the certifying compilation approach to code generation and focus on the implementation and practical issues. It turns out that the checking of the certificates is the actual bottleneck of certifying compilation. We present a proof schema to overcome this bottleneck. Hence we show the applicability of the certifying compilation approach for small sized programs processed by a compiler's code generation phase.     

A linear algorithm for MLL proof net correctness and sequentialization

The paper presents in full detail the first linear algorithm given in the literature (Guerrini (1999) [6]) implementing proof structure correctness for multiplicative linear logic without units. The algorithm is essentially a reformulation of the Danos contractibility criterion in terms of a sort of unification. As for term unification, a direct implementation of the unification criterion leads to a quasi-linear algorithm. Linearity is obtained after observing that the disjoint-set union-find at the core of the unification criterion is a special case of union-find with a real linear time solution.     

A Complete Mechanization of Correctness of a String-Preprocessing Algorithm

We report on mechanization of a correctness proof of a string-preprocessing algorithm. This preprocessing algorithm is employed in Boyer-Moore’s pattern matching algorithm. The mechanization is carried out using the PVS system. The correctness proof being mechanized has been formulated in Linear Time Temporal Logic. It consists of fourteen lemmata which are related to safety properties and two additional lemmata dealing with liveness properties. The entire mechanization of the safety and liveness parts has been completed. Several small errors and omissions were found in the handwritten proof and corrected. Yet, the manual correctness proof of the string-preprocessing algorithm was found to satisfy the usual mathematical validity. We conclude that the string-preprocessing algorithm in Boyer-Moore’s pattern matching algorithm, corrected a number of times because of flaws, does not contain any more undiscovered errors. An extended abstract of this work appears in the Proceedings of the 8^th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS ‘02).     

Structure sharing for quantified terms: Fundamentals

Structure sharing is used in symbolic computation to share a common top level between terms with different lower levels. It is widely used in the implementation of Prolog interpreters and is of interest for the implementation of automatic theorem provers, interactive proof editors and verification systems. Previously, structure sharing has been applied only to free-variable terms. In this paper we extend the structure sharing technique to quantified terms. We give an efficient unification algorithm of our structure sharing representation of quantified terms, and we prove the correctness of the algorithm.     

An incremental garbage collection algorithm for multi-mutator systems

An elementary correctness proof for Ben-Ari's algorithm (1984) for incremental garbage collection is given. We give a new algorithm for systems in which there are multiple mutators and a proof of its correctness, which is a minor modification of the previous proof. Finally, we remark upon a way to implement these algorithms that may increase their performance on certain architectures. Carl Pixley holds B.S., M.S. and Ph.D. degrees in mathematics from the University of Omaha, Rutgers-The State University, and the State University of New York at Binghamton, respectively. His principal contributions are the Pixley-Roy construction of set-theoretic topology, a example in the selection theory of infinite-dimensional spaces, a decomposition theorem (with W. Eaton) in geometric topology, and the design and implementation of demanddriven arithmetic in a functional programming language. He is now a member of the technical staff of the VLSI Computer Aided Design Program of Microelectronics and Computer Technology Corporation (MCC) in Austin Texas, where he is investigating mathematical methods in the verification of hardware.     

Theorem Proving Guided Development of Formal Assertions in a Resource-Constrained Scheduler for High-Level Synthesis

This paper presents a formal specification and a proof of correctness for the widely-used Force-Directed List Scheduling (FDLS) algorithm for resource-constrained scheduling of data flow graphs in high-level synthesis systems. The proof effort is conducted using a higher-order logic theorem prover. During the proof effort many interesting properties of the FDLS algorithm are discovered. These properties are formally stated and proved in a higher-order logic theorem proving environment. These properties constitute a detailed set of formal assertions and invariants that should hold at various steps in the FDLS algorithm. They are then inserted as programming assertions in the implementation of the FDLS algorithm in a production-strength high-level synthesis system. When turned on, the programming assertions (1) certify whether a specific run of the FDLS algorithm produced correct schedules and, (2) in the event of failure, help discover and isolate programming errors in the FDLS implementation.We present a detailed example and several experiments to demonstrate the effectiveness of these assertions in discovering and isolating errors. Based on this experience, we discuss the role of the formal theorem proving exercise in developing a useful set of assertions for embedding in the scheduler code and argue that in the absence of such a formal proof checking effort, discovering such a useful set of assertions would have been an arduous if not impossible task.     

Systematic formal verification for fault-tolerant time-triggeredalgorithms

Many critical real-time applications are implemented as time-triggered systems. We present a systematic way to derive such time-triggered implementations from algorithms specified as functional programs (in which form their correctness and fault-tolerance properties can be formally and mechanically verified with relative ease). The functional program is first transformed into an untimed synchronous system and, then, to its time-triggered implementation. The first step is specific to the algorithm concerned, but the second is generic and we prove its correctness. This proof has been formalized and mechanically checked with the PVS verification system. The approach provides a methodology that can ease the formal specification and assurance of critical fault-tolerant systems     

Using simulated execution in verifying distributed algorithms

This paper presents a methodology for using simulated execution to assist a theorem prover in verifying safety properties of distributed systems. Execution-based techniques such as testing can increase confidence in an implementation, provide intuition about behavior, and detect simple errors quickly. They cannot by themselves demonstrate correctness. However, they can aid theorem provers by suggesting necessary lemmas and providing tactics to structure proofs. This paper describes the use of these techniques in a machine-checked proof of correctness of the Paxos algorithm for distributed consensus .     

A Traffic Partition Algorithm for Switched LANs and Its Performance Analysis

An algorithm is proposed which can be used for the topology design of switched LAN with heavy traffic and multi-segments.The main principle of the algorithm is to split the whole traffic to segments as even as possible.The algorithm consists of binary division and ordinary division.When the number of segments equals to powers of 2,binary division is used;ordinary division is based on binary division but suitable to more common cases.Both correctness and time complexity of the algorithm are discussed in detail,and a comparison of the algorithm with the best result is given at the same time.     

A mechanical proof of Segall's PIF algorithm

We describe the construction of a distributed algorithm with asynchronous communication together with a mechanically verified proof of correctness. For this purpose we treat Segall's PIF algorithm (propagation of information with feedback). The proofs are based on invariants, and variant functions for termination. The theorem prover NQTHM is used to deal with the many case distinctions due to asynchronous distributed computation. Emphasis is on the modelling assumptions, the treatment of nondeterminacy, the forms of termination detection, and the proof obligations for a complete mechanical proof. Finally, a comparison is made with (the proof of) the minimum spanning tree algorithm of Gallager, Humblet, and Spira, for which the technique was developed.