What's a reasonable proof strategy to formally verify Ukkonen's algorithm in, say, Coq? The ingredients as far as I can tell would be:

  1. some form of separation logic to be able to reason about the state of the array as we are building up the data
  2. separation logic to reason about suffix links and their validity
  3. LOTS OF case analysis to prove that the invariants hold?? For example, this paper on 'Efficient Representation for Online Suffix Tree Construction' lists the cases in Ukkonen's algorithm --- this lists heavy cases anysis.

The #3 is the most finicky part of the whole enterprise; It seems like there ought to be a more 'principled' way to build the algorithm rather than the monolithic all-or-nothing proofs that we currently see?

  • 1
    $\begingroup$ It sounds like you're asking for a more principled paper proof first! $\endgroup$ – cody Feb 15 '20 at 15:49
  • $\begingroup$ Yes :) So do you know a more principled proof on paper? $\endgroup$ – Siddharth Bhat Feb 15 '20 at 15:59
  • 1
    $\begingroup$ Sadly, I do not. $\endgroup$ – cody Feb 16 '20 at 18:11

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.