# A reasonable proof strategy for formally verifying Ukkonen's algorithm?

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