Lab for Automated Reasoning and Analysis 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]]
 
sav07_lecture_15_skeleton.txt · Last modified: 2007/05/07 10:56 by vkuncak
 
© EPFL 2018 - Legal notice