*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Formally proving the Boyer text matching algorithm*From*: Lars Noschinski <noschinl at in.tum.de>*Date*: Wed, 28 Aug 2013 15:59:26 +0200*In-reply-to*: <A0CA4F54-0440-4E26-B943-978F52336E5D@gmail.com>*References*: <CABCjkDpsgdwyWu6vbCc4dKPuepxCA1+6psjOOW4J38zO8x3VkA@mail.gmail.com> <F5283140-7DAF-42A6-94F9-22527CF774AA@gmail.com> <CABCjkDo7d6=V=iRSzbHmACL6xVN-UbCCrASL7ddLTJ7gJJPRzQ@mail.gmail.com> <A0CA4F54-0440-4E26-B943-978F52336E5D@gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:10.0.12) Gecko/20130116 Icedove/10.0.12

On 28.08.2013 01:20, Jasmin Blanchette wrote:

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.

[1] http://ssrg.nicta.com.au/projects/TS/autocorres/ -- Lars

**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

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

- Previous by Date: Re: [isabelle] Kleene's Ternary Logic
- Next by Date: [isabelle] Research Fellow Position Birmingham
- 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