Prague Stringology Conference 2014
Bruce W. Watson, Loek Cleophas and Derrick G. Kourie
Using Correctness-by-Construction to Derive Dead-zone Algorithms
| Abstract: |
| We give a derivation, in the form of a stepwise (refinement-oriented) presentation, of a family of algorithms for single keyword pattern matching, all based on the so-called dead-zone algorithm-style, in which input text parts are tracked as either unprocessed (‘live’), or processed (‘dead’). Such algorithms allow for Boyer-Moore-style shifting in the input in two directions (left and right) instead of one, and have shown promising results in practice. The algorithms are the more interesting because of their potential for concurrency (multithreading). The focus of our algorithm family presentation is on correctness-arguments (proofs) accompanying each step, and on the resulting elegance and efficiency. Several new algorithms are described as part of this algorithm family, including ones amenable to using concurrency. |
| Download paper: |  |
 |
 |
| PostScript | BibTeX reference |
| Download presentation: |  |