Email Gateway (Aug 19 2022 at 11:44): Email Gateway (Aug 19 2022 at 11:44):From: li yongjian <lyj238@gmail.com>
Dear Isabelle experts:
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?
If there is no such work, can someone point the hints of using some
available theories to prove it?
Thanks in advance?
regards!
best?
Email Gateway (Aug 19 2022 at 11:44):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Dear Yongjian,
The Moore in Boyer-Moore did a proof in ACL2:
http://www.cs.utexas.edu/~moore/publications/moore-martinez-09.pdf
This might very well be the only formal correctness proof of this algorithm.
Regards,
Jasmin
Email Gateway (Aug 19 2022 at 11:44):From: li yongjian <lyj238@gmail.com>
Hi, Jasmin Blanchette:
thanks.
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?
lyj
Email Gateway (Aug 19 2022 at 11:44):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Dear Yongjian,
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/
Email Gateway (Aug 19 2022 at 11:45):From: Lars Noschinski <noschinl@in.tum.de>
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
Last updated: Nov 21 2024 at 12:39 UTC