*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*: Wed, 28 Aug 2013 01:20:43 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <CABCjkDo7d6=V=iRSzbHmACL6xVN-UbCCrASL7ddLTJ7gJJPRzQ@mail.gmail.com>*References*: <CABCjkDpsgdwyWu6vbCc4dKPuepxCA1+6psjOOW4J38zO8x3VkA@mail.gmail.com> <F5283140-7DAF-42A6-94F9-22527CF774AA@gmail.com> <CABCjkDo7d6=V=iRSzbHmACL6xVN-UbCCrASL7ddLTJ7gJJPRzQ@mail.gmail.com>

Dear Yongjian, > 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? Gerwin Klein's group at NICTA have developed a tool that integrates C with Simpl [1]. Perhaps that's what you are referring to by "C-based proof theory such as Simpl". It should indeed be possible to verify the C code of Boyer-Moore that way. Perhaps those who know the tool better can comment further on its use. Regards, Jasmin [1] http://ssrg.nicta.com.au/software/TS/c-parser/

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

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

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

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

- Previous by Date: Re: [isabelle] Formally proving the Boyer text matching algorithm
- 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