Introduction to using MSOL over strings to verify linked data structures
Here is a simple linked list operation in Jahob.
What do verification conditions look like?
tree [Node.next] --> F(Node.next)
I will describe a decision procedure that can decide such formulas.