Actualités
  Période
semaine
ou mois
aucune période


  Thèmes:
Thèses
Colloques
Autres
Groupes
Tous les thèmes

   
  Liens:
Voir les thèses

Voir les colloques

Voir les autres événements

Voir la page des groupes

Accéder à l'intranet

Intitulé:   
Split-width technique for the verification of concurrent programs with data structures
du groupe Modélisation et Verification

Date 2013-06-20  11:30-12:30
TitreSplit-width technique for the verification of concurrent programs with data structures 
RésuméWe consider systems of concurrent boolean programs equipped with several data structures. The data structures can be unbounded stacks or unbounded queues. Each data structure allows write access to only one process (call it writer), and read access to only one (possibly different) process (call it reader). A stack whose writer and reader are the same corresponds to an unbounded local stack of the writer. A queue serves as an unbounded reliable FIFO channel from its writer to its reader. As these systems are very powerful, they render most verification problems undecidable. We introduce a parameter called split-width for its under-approximate verification. Split-width is a notion similar to tree-width, but more handy for the systems we consider. Restricting to bounded split-width behaviors gives an EXPTIME decision procedure for model checking these systems against temporal logics and propositional dynamic logics, and a decision procedure for model checking against MSO. We show that split-width can capture several interesting and relaxed scheduling policies. This is a joint work with Paul Gastin and K. Narayan Kumar.  
Lieu076 
OrateurAiswarya Cyriac 
Emailaiswarya.cyriac@lsv.ens-cachan.fr 
UrlLSV 



Aucun document lié à cet événement.

Retour
Retour à l'index