LARA Encoding Lists using WS1S 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/ Field constraint analysis Pointer Assertion Logic Engine