Differences

This shows you the differences between two versions of the page.

--- sav07_lecture_15_skeleton [2007/05/06 20:54]
vkuncak
+++ sav07_lecture_15_skeleton [2007/05/07 10:56]
vkuncak
@@ Line 1: / Line 1: @@
 ====== Finite state machines and verification of programs that manipulate linked lists ======
-Consider programs that manipulate linked lists.
+  * [[Introduction to using MSOL over strings to verify linked lists]]
-Here is one example, verified using Jahob:
-We can generate verification conditions that say that if the initial data structure is a list the desired properties hold.  These properties can talk about reachability in the list.
-We show in this lecture how we can prove such verification conditions using a very expressive logic, 'weak monadic second-order logic of one successor'.
   * [[Strings and languages]]
@@ Line 25: / Line 19: @@
   * [[Expressing regular expressions in MSOL over strings]]
-References:
+===== References =====
+Automata and languages:
+  * [[http://www-math.mit.edu/~sipser/book.html|Introduction to the Theory of Computation]]
+  * [[http://infolab.stanford.edu/~ullman/ialc.html|Introduction to Automata Theory, Languages, and Computation]]
+MSOL:
   * [[http://www.grappa.univ-lille3.fr/tata/|Tree Automata Techniques and Applications (Tata book)]]
   * [[http://www.brics.dk/mona/|The MONA Project]]
   * [[http://www.irisa.fr/lande/genet/timbuk/|Timbook for Reachability Analysis and Tree Automata Calculations]]
-  * [[http://infolab.stanford.edu/~ullman/ialc.html|Introduction to Automata Theory, Languages, and Computation]]
+Verification of linked structures using automata or MSOL:
+  * [[http://lara.epfl.ch/~kuncak/papers/WiesETAL06FieldConstraintAnalysis.html|Field constraint analysis]]
+  * [[http://www.brics.dk/PALE|Pointer Assertion Logic Engine]]