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 . 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, 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)
This archive was generated by a fusion of
Pipermail (Mailman edition) and