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



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/


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