LARA This is an old revision of the document! Encoding lists using MSOL over strings References Verification via structure simulation