*To*: li yongjian <lyj238 at gmail.com>*Subject*: Re: [isabelle] Formally proving the Boyer text matching algorithm*From*: Jasmin Blanchette <jasmin.blanchette at gmail.com>*Date*: Tue, 27 Aug 2013 17:26:38 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <CABCjkDpsgdwyWu6vbCc4dKPuepxCA1+6psjOOW4J38zO8x3VkA@mail.gmail.com>*References*: <CABCjkDpsgdwyWu6vbCc4dKPuepxCA1+6psjOOW4J38zO8x3VkA@mail.gmail.com>

Dear Yongjian, > Boyer text matching algorithm is a widely-used. See > http://en.wikipedia.org/wiki/Boyer%E2%80%93Moore_string_search_algorithm. > Do anyone have tried to prove its correctness by theorem proving. > Or do some similar work? The Moore in Boyer-Moore did a proof in ACL2: http://www.cs.utexas.edu/~moore/publications/moore-martinez-09.pdf This might very well be the only formal correctness proof of this algorithm. Regards, Jasmin

**Follow-Ups**:**Re: [isabelle] Formally proving the Boyer text matching algorithm***From:*li yongjian

**References**:**[isabelle] Formally proving the Boyer text matching algorithm***From:*li yongjian

- Previous by Date: [isabelle] Formally proving the Boyer text matching algorithm
- Next by Date: Re: [isabelle] Ordinal of a datatype instantiated to enum
- Previous by Thread: [isabelle] Formally proving the Boyer text matching algorithm
- Next by Thread: Re: [isabelle] Formally proving the Boyer text matching algorithm
- Cl-isabelle-users August 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list