loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Eighth IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'02)
Mechanization of a Proof of String-Preprocessing in Boyer-Moore?s Pattern Matching Algorithm
Greenbelt, Maryland
December 02-December 04
ISBN: 0-7695-1757-9
ASCII Text
x 
 
Miloslav Besta, Frank Stomp, "Mechanization of a Proof of String-Preprocessing in Boyer-Moore?s Pattern Matching Algorithm," Engineering of Complex Computer Systems, IEEE International Conference on, pp. 68, Eighth IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'02), 2002.
 
 
BibTex
x
 
@article{ 10.1109/ICECCS.2002.1181499,
author = {Miloslav Besta and Frank Stomp},
title = {Mechanization of a Proof of String-Preprocessing in Boyer-Moore?s Pattern Matching Algorithm},
journal ={Engineering of Complex Computer Systems, IEEE International Conference on},
volume = {0},
year = {2002},
issn = {1050-4729},
pages = {68},
doi = {http://doi.ieeecomputersociety.org/10.1109/ICECCS.2002.1181499},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Engineering of Complex Computer Systems, IEEE International Conference on
TI - Mechanization of a Proof of String-Preprocessing in Boyer-Moore?s Pattern Matching Algorithm
SN - 1050-4729
SP
EP
A1 - Miloslav Besta,
A1 - Frank Stomp,
PY - 2002
KW - null
VL - 0
JA - Engineering of Complex Computer Systems, IEEE International Conference on
ER -
 
Miloslav Besta, Wayne State University
Frank Stomp, Wayne State University
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.
Citation:
Miloslav Besta, Frank Stomp, "Mechanization of a Proof of String-Preprocessing in Boyer-Moore?s Pattern Matching Algorithm," iceccs, pp.68, Eighth IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'02), 2002
Usage of this product signifies your acceptance of the Terms of Use.