Lab for Automated Reasoning and Analysis LARA

Introduction to using MSOL over strings to verify linked data structures

Here is a simple linked list operation in Jahob.

What do verification conditions look like?

tree [Node.next] --> F(Node.next)

I will describe a decision procedure that can decide such formulas.

 
introduction_to_using_msol_over_strings_to_verify_linked_lists.txt · Last modified: 2007/05/14 12:02 by vkuncak