<p>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:</p>

<ol>
<li>some form of separation logic to be able to reason about the state of the array as we are building up the data</li>
<li>separation logic to reason about suffix links and their validity</li>
<li>LOTS OF case analysis to prove that the invariants hold?? For example, <a href="https://arxiv.org/pdf/1403.0457.pdf" rel="nofollow noreferrer">this paper on 'Efficient Representation for Online Suffix Tree Construction'</a> lists the cases in Ukkonen's algorithm --- this lists heavy cases anysis.</li>
</ol>

<p>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?</p>

CC BY-SA 4.0
2020-02-15T15:49:13.170Z
It sounds like you're asking for a more principled paper proof first!
cody
CC BY-SA 4.0
2020-02-15T15:59:37.577Z
Yes :) So do you know a more principled proof on paper?
Siddharth Bhat
CC BY-SA 4.0
2020-02-16T18:11:47.203Z
Sadly, I do not.
cody
<automated-theorem-proving><formal-methods><string-search>
A reasonable proof strategy for formally verifying Ukkonen's algorithm?
Siddharth Bhat
# A reasonable proof strategy for formally verifying Ukkonen's algorithm?

(Asked by: username_0 on 2020-02-13)

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'](https://arxiv.org/pdf/1403.0457.pdf) 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?

**Tags:** automated-theorem-proving, formal-methods, string-search
> **Comments:**
> **username_1**: It sounds like you're asking for a more principled paper proof first!  
> **username_0**: Yes :) So do you know a more principled proof on paper?  
> **username_1**: Sadly, I do not.  

---

## 0 answers

