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



On 28.08.2013 01:20, Jasmin Blanchette wrote:
   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.

There is also David Greenaway's autocorres tool[1], which is based on top of said tool. It abstracts a bit more from the raw transformation done by the C parser (and I think there is new release coming soon).

Be warned that the verification of C code is a lot more work than verifying an abstract implementation. When verifying some graph-related algorithm written in C with the help of autocorres, I found it very helpful to refine the program to something more abstract (and wrote a lot of rules to facilitate this)

[1] http://ssrg.nicta.com.au/projects/TS/autocorres/

  -- Lars




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