Re: [isabelle] Formally proving the Boyer text matching algorithm
> 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 . 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and