Title :
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
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;
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
DOI :
10.1109/ICECCS.2002.1181499
