Parameterized refinement is a refinement technique for preserving specific linear time temporal logic properties during formal program development. In this paper, we describe a proof method for verifying that one program is a parameterized refinement of another program. Our method combines transduction, due to Jonsson, Pnueli, and Rump, for showing that one system simulates another system, with techniques used in implementations of model checkers. The method is argued to be attractive in a development environment, where tools such as model checkers are applied. It enables rigorous verification that one system is a parameterized refinement of another system.

We report on a mechanization of a correctness proof of a string-preprocessing algorithm. This preprocessing algorithm is employed in Boyer-Moore's (1977) 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. We mainly focus on mechanization of the safety part. In a future paper we will address our proof of the liveness part in more detail.

This paper proposes a new approach and new techniques for online monitoring of concurrent programs to ensure that some of their safety properties are not violated. The techniques modify erroneous systems which violate a certain safety property, into new systems which satisfy the safety property by adding a new layer that controls the scheduling of steps in the system. We formally characterize the relationship between the erroneous and the new system. Safety monitors for mutual-exclusion, l-exclusion, and the producer consumer tasks are presented. A proof for the mutual-exclusion task is presented to demonstrate the applicability of our approach. Our results are also of significance in the context of evolving systems, systems which are repeatedly modified due to changes in the user requirements, user specifications, or implementation. The monitoring technique proposed ensures that safety requirements are not violated in such evolving systems, in spite of frequent changes.

Abstract. SCI – Scalable Coherent Interface – is an IEEE standard for specifying communication between multiprocessors in a shared memory model. In this paper we model part of SCI by a program written in a UNITY-like programming language. This part of SCI is formally specified in Manna and Pnueli's Linear Time Temporal Logic (LTL). We give a sketch of our proof that the program satisfies its specification. The proof has been carried out within LTL. It uses history variables. Structuring of the proof has been achieved by careful formulation of lemmata and the use of auxiliary predicates as an abstraction mechanism.

The problem of computing with faulty shared bits is addressed. The focus is on constructing a reliable test&set bit from a collection of test&set bits of which some may be faulty. Faults are modeled by allowing operations on the faulty bits to return a special distinguished value, signaling that the operation may not have taken place. Such faults are called omission faults. Some of the constructions are required to be gracefully degrading for omission. That is, if the bound on the number of component bits which fail is exceeded, the constructed bit may suffer faults, but only faults which are no more severe than those of the components; and the constructed bit behaves as intended if the number of component bits which fail does not exceed that bound. Several efficient constructions are presented, and bounds on the space required are given. Our constructions for omission faults also apply to other fault models.

The problem of computing with faulty shared bits is addressed. The focus is on constructing a reliable tests and the constructed bit behaves as intended if the number of component bits which fail does not exceed that bound. Several efficient constructions are presented, and bounds on the space required are given. Our constructions for omission faults also apply to other fault models.

Abstract Designers of network algorithms often give elegant informal descriptions of the intuition behind their algorithms (see [ GHS83 , Hum83 , MeS79 , Seg82 , Seg83 , ZeS80 ]). Usually these descriptions are structured as if subtasks are performed one after the other. Although these subtasks are performed sequentially from a logical point of view, they are performed concurrently from an operational point of view. The current paper presents a principle for formally designing and verifying these kinds of algorithms. It is formulated in Manna and Pnueli’s linear time temporal logic [ MaP83 , MaP92 ]. This principle is applicable to large classes of algorithms, such as those for computing minimum-paths, connectivity, network flow, and minimum-weight spanning trees.

Abstract Highly optimised algorithms are, in general, hard to understand. This is a consequence of the designer's sacrifice of clarity and modularity in favour of efficiency. In this paper we present a formal derivation of a rather ingenious algorithm, viz., the fast pattern matching algorithm of Boyer and Moore. The development illustrates that transformational programming combined with assertional reasoning provides an appropriate approach for developing and understanding highly optimised algorithms.