Consider programs that manipulate linked lists.

Here is one example, verified using Jahob:

We can generate verification conditions that say that if the initial data structure is a list the desired properties hold. These properties can talk about reachability in the list.

We show in this lecture how we can prove such verification conditions using a very expressive logic, 'weak monadic second-order logic of one successor'.

• Strings and languages

• Finite state machine
• Determinization of finite state machine
• Finite state machine with epsilon transitions
• Closure properties of finite state machines
• Regular expression
• Equivalence of finite state machine and regular expression languages

• Using automata to decide Presburger arithmetic
• MSOL over strings
• Using automata to decide MSOL over finite strings
• Regular expressions for automata with parallel inputs
• Expressing finite automata in MSOL over strings
• Expressing regular expressions in MSOL over strings

Automata and languages:

• Introduction to the Theory of Computation
• Introduction to Automata Theory, Languages, and Computation

MSOL:

• Tree Automata Techniques and Applications (Tata book)
• The MONA Project
• Timbook for Reachability Analysis and Tree Automata Calculations

Verification of linked structures using automata or MSOL:

• Field constraint analysis
• Pointer Assertion Logic Engine