Mechanization of a Proof of String-Preprocessing in Boyer-Moore's Pattern Matching Algorithm

We report on a 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. In this paper 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.