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

Hi, Jasmin Blanchette:
  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?


On Tue, Aug 27, 2013 at 11:26 PM, Jasmin Blanchette <
jasmin.blanchette at> wrote:

> Dear Yongjian,
> >   Boyer text matching algorithm  is a widely-used. See
> >
> .
> >   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:
> 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.