Mechanization of a proof of string-preprocessing in Boyer-Moore´s pattern matching algorithm

Author

Besta, Miloslav ; Stomp, Frank

Author_Institution

Dept. of Comput. Sci., Wayne State Univ., Detroit, MI, USA

fYear

2002

fDate

2-4 Dec. 2002

Firstpage

68

Lastpage

77

Abstract

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.

Keywords

formal specification; program verification; string matching; temporal logic; theorem proving; Linear Time Temporal Logic; PVS system; Prototype Verification System; algorithm correctness proof; liveness properties; pattern matching algorithm; safety properties; string preprocessing proof; Computer science; Error correction; Formal specifications; Logic; Pattern matching; Safety;

fLanguage

English

Publisher

ieee

Conference_Titel

Engineering of Complex Computer Systems, 2002. Proceedings. Eighth IEEE International Conference on

Conference_Location

Greenbelt, MD, USA

Print_ISBN

0-7695-1757-9

Type

conf

DOI

10.1109/ICECCS.2002.1181499

Filename

1181499