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 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:
> This might very well be the only formal correctness proof of this
This archive was generated by a fusion of
Pipermail (Mailman edition) and