|
Evènement pour le groupe Modélisation et Verification
Date | 2012-05-03 11:30-12:30 |
Titre | Bounded 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. |
Lieu | 076 |
Orateur | Michael Emmi |
Email | michael.emmi@liafa.jussieu.fr |
Url | LIAFA, Paris |
Aucun document lié à cet événement. RetourRetour à l'index
| |