LARA This is an old revision of the document! Encoding lists using MSOL over strings Example file 'MONA' tool: slist-mona.txt How to encode multiple lists How to encode doubly-linked lists cyclic lists References Verification via structure simulation Field constraint analysis Pointer Assertion Logic Engine