*To*: Jasmin Blanchette <jasmin.blanchette at gmail.com>*Subject*: Re: [isabelle] Formally proving the Boyer text matching algorithm*From*: li yongjian <lyj238 at gmail.com>*Date*: Wed, 28 Aug 2013 07:08:14 +0800*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <F5283140-7DAF-42A6-94F9-22527CF774AA@gmail.com>*References*: <CABCjkDpsgdwyWu6vbCc4dKPuepxCA1+6psjOOW4J38zO8x3VkA@mail.gmail.com> <F5283140-7DAF-42A6-94F9-22527CF774AA@gmail.com>

Hi, Jasmin Blanchette: thanks. I have a further question. If I hace a C code for Boyer text matching algorithm, can I use the C-based proof theory such as Simpl to prove the c-code's correctness? lyj On Tue, Aug 27, 2013 at 11:26 PM, Jasmin Blanchette < jasmin.blanchette at gmail.com> wrote: > 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:*Jasmin Blanchette

**Re: [isabelle] Formally proving the Boyer text matching algorithm***From:*lyj238

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

**Re: [isabelle] Formally proving the Boyer text matching algorithm***From:*Jasmin Blanchette

- Previous by Date: Re: [isabelle] Ordinal of a datatype instantiated to enum
- Next by Date: Re: [isabelle] Formally proving the Boyer text matching algorithm
- Previous by Thread: Re: [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