LARA 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: http://lara.epfl.ch/~kuncak/jahob/ds/CircularList/ References Verification via structure simulation Field constraint analysis Pointer Assertion Logic Engine
