|
SVA: using CSP to analyse shared variable programs| old_uid | 9499 |
|---|
| title | SVA: using CSP to analyse shared variable programs |
|---|
| start_date | 2011/01/11 |
|---|
| schedule | 14h-15h |
|---|
| online | no |
|---|
| location_info | bat 25/26, salle 105 |
|---|
| summary | SVA is a new tool developed by me and David Hopkins that translates a shared variable program into Hoare's CSP and analyses it on FDR. ÊI will discuss how this translation is done, the great effectiveness of FDR's compression functions on the result and a model of refinement between shared variable program fragments. As examples I will solve an open problem regarding Simpson's 4-slot algorithm and show how a finite model checking run can prove the bakery algorithm for an unbounded ticket type and an arbitrary number of nodes.
This talk is based on Chapters 18 and 19 of my new book "Understanding Concurrent Systems". |
|---|
| responsibles | Baerecke |
|---|
| |
|