On obtaining the Boyer-Moore string-matching algorithm by partial evaluation

We present the first derivation of the search phase of the Boyer-Moore string-matching algorithm by partial evaluation of an inefficient string matcher. The derivation hinges on identifying the bad-character-shift heuristic as a binding-time improvement, bounded static variation. An inefficient string matcher incorporating this binding-time improvement specializes into the search phase of the Horspool algorithm, which is a simplified variant of the Boyer-Moore algorithm. Combining the bad-character-shift binding-time improvement with our previous results yields a new binding-time-improved string matcher that specializes into the search phase of the Boyer-Moore algorithm.     

Assertion checking environment (ACE) for formal verification of C programs

In this paper we describe an Assertion Checking Environment (ACE) for compositional verification of programs, which are written in an industrially sponsored safe subset of C programming language called MISRA C [Guidelines for the Use of the C Language in Vehicle Based Software, 1998]. The theory is based on Hoare logic [Commun. ACM 12 (1969) 576] and the C programs are verified using static assertion checking technique. First the functional specifications of the program, captured in the form of pre- and post-conditions for each C function, are derived from the specifications. These pre- and post-conditions are then introduced as assertions (also called annotations or formal comments) in the program code. The assertions are then proved formally using ACE and theorem proving tool called Stanford Temporal Prover [The Stanford Temporal Prover User's Manual, 1998]. ACE has been developed by us and consists mainly of a translator c2spl, a GUI and some utility programs. The technique and tools developed are targeted towards verification of real-time embedded software.     

钟罩式气体流量标准装置不确定度分析

介绍了钟罩式气体流量标准装置的几种检定方法,比较了各检定方法的区别、特点及要求,并结合检定数据进行了不确定度分析。     

A mechanically verified incremental garbage collector

As an application of a system designed for concurrent program verification, we describe a formalisation and mechanical proof of the correctness of Ben-Ari's incremental garbage collection algorithm. The proof system is based on the Manna-Pnueli model of concurrency and is implemented as an extension of the Boyer-Moore prover. The correctness of the garbage collector is represented by two theorems, stating a) that nothing except garbage is ever collected (safety), and b) that all garbage is eventually collected (liveness). We compare our mechanised treatment with several published proofs of the same results.     

Improved string searching

We show that it is possible to improve the average time of the Boyer-Moore string matching algorithm using more space. This is accomplished by applying a transformation that virtually increases the size of the alphabet in use. The improvement is such that for long patterns it is possible to obtain an algorithm more than 50 per cent faster than the original one. We include experimental results on random and English text. Some improvements for searching on English text are also discussed.     

面向入侵检测的模式匹配算法研究

在入侵检测系统的实现中,关键部分是检测引擎的实现。而在检测引擎的实现中,关键的是数据分析模块。对于基于规则的入侵检测来说,模式匹配算法非常重要,它直接影响到系统的准确性和实时性能。论文主要研究了BruteForce算法,Boyer-Moore算法,Aho-Corasick算法,Set-wiseBoyer-Moore-Horspool算法,Aho-Corasick_Boyer-Moore算法。     

The Tail-Recursive SECD Machine

One method for producing verified implementations of programming languages is to formally derive them from abstract machines. Tail-recursive abstract machines provide efficient support for iterative processes via the ordinary procedure call mechanism. This document argues that the use of tail-recursive abstract machines incurs only a small increase in theorem-proving burden when compared with what is required when using ordinary abstract machines. The position is supported by comparing correctness proofs performed using the Boyer–Moore theorem prover.A by-product of this effort is a syntactic criterion based on tail contexts for identifying which procedure calls must be implemented as tail calls. The concept of tail contexts was used in the latest Scheme Report, the only language specification known to the author that defines the requirement that its implementations must be tail recursive.     

Exploitation of parallel processing for implementing high-performance deduction systems

We describe a scheme for parallelizing first-order logic deduction systems. This scheme has been successfully used for parallelizing OTTER, which is a sequential deduction system developed at Argonne National Laboratory. This parallel deduction system, called PARRallel OTter-II (PARROT-II) has attained real speedups in excess of 20 over the best results of current sequential deduction systems. We believe that our results are of interest for two distinct reasons: (1) this is (as far as we know) the first case in which a system has successfully exploited parallelism to outperform the best sequential deduction systems on difficult problems, and (2) we believe that our approach generalizes to other deduction paradigms (e.g., term rewriting systems).This paper discusses the motivation for developing the scheme used by PARROT-II and the implementation details of PARROT-II. It also presents timing results for PARROT-II for some benchmark problems.Work submitted as partial fulfillment of the requirements for the doctoral degree at the Graduate College of the University of Illinois at Chicago. This work was supported in part by the Applied Mathematical Sciences subprogram of the Office of Energy Research, U.S. Department of Energy, under Contract W-31-109-Eng-38.     

Fast string searching

Since the Boyer-Moore algorithm was described in 1977, it has been the standard benchmark for the practical string search literature. Yet this yardstick compares badly with current practice. We describe two algorithms that perform 47% fewer comparisons and are about 4.5 times faster across a wide range of architectures and compilers. These new variants are members of a family of algorithms based on the skip loop structure of the preferred, but often neglected, fast form of Boyer-Moore. We present a taxonomy for this family, and describe a toolkit of components that can be used to design an algorithm most appropriate for a given set of requirements.     

On tuning the boyer-moore-horspool string searching algorithm

Experiments suggest that recently reported improvements to the Boyer-Moore-Horspool string searching algorithm may be due to compiler effects rather than to properties of the language being searched.