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:
- some form of separation logic to be able to reason about the state of the array as we are building up the data
- separation logic to reason about suffix links and their validity
- 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?