A sequel to SAV07 Lecture 16 and SAV07 Lecture 15.

Preliminary reading:

• Tree Automata Techniques and Applications (Tata book), pages 13-20
• http://www.brics.dk/mona/papers/implementation-secrets/journal.pdf

Topics to cover:

• 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

• Encoding lists using MSOL over strings
• Tree automata

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

More

• Constraint solving and decision problems of first-order theories of concrete domains, by Ralf Treinen
• Efficient Static Analysis of XML Paths and Types