LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
sav07_lecture_15_skeleton [2007/05/07 10:36]
vkuncak
sav07_lecture_15_skeleton [2007/05/07 10:56] (current)
vkuncak
Line 1: Line 1:
 ====== Finite state machines and verification of programs that manipulate linked lists ====== ====== 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]]   * [[Strings and languages]]