*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Formally proving the Boyer text matching algorithm*From*: li yongjian <lyj238 at gmail.com>*Date*: Tue, 27 Aug 2013 23:06:50 +0800

Dear Isabelle experts: 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? If there is no such work, can someone point the hints of using some available theories to prove it? Thanks in advance? regards! best?

**Follow-Ups**:**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] Ordinal of a datatype instantiated to enum
- 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