Evènement pour le groupe Modélisation et Verification


Date 2012-05-03  11:30-12:30
TitreBounded Phase Analysis of Message-Passing Programs 
RésuméWe describe a novel technique for bounded analysis of asynchronous message-passing programs with ordered message queues. Our bounding parameter does not limit the number of pending messages, nor the number of “contexts-switches” between processes. Instead, we limit the number of process communication cycles, in which an unbounded number of messages are sent to an unbounded number of processes across an unbounded number of contexts. We show that remarkably, despite the potential for such vast exploration, our bounding scheme gives rise to a simple and efficient program analysis by reduction to sequential programs. As our reduction avoids explicitly representing message queues, our analysis scales irrespectively of queue content and variation. 
Lieu076 
OrateurMichael Emmi 
Emailmichael.emmi@liafa.jussieu.fr 
UrlLIAFA, Paris 



Aucun document lié à cet événement.

Retour
Retour à l'index