LARA

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.