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



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



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.