|
Evènement pour le groupe Modélisation et Verification
Date | 2009-05-14 11:00-12:15 |
Titre | What's decidable for Asynchronous Programs ? |
Résumé | An asynchronous or "event-driven'' program is one that contains
procedure calls which are not directly executed from the call site,
but stored and executed later by an external scheduler.
By providing a low-overhead way to manage concurrent interactions,
asynchronous programs form the core of many server programs, embedded
systems, and popular programming styles for the web (Ajax).
Unfortunately, such programs can be hard to write and maintain as
sequential control flow needs to be split into several disjoint
handlers.
They are a challenge for static analysis tools as they are infinite
state: both the program stack and the number of outstanding
asynchronous requests may be unbounded.
We show that safety and liveness properties can be checked effectively
for the class of Boolean asynchronous programs, thus enabling
automatic static techniques to check for correctness or for errors. |
Lieu | Salle 076, LaBRI, Rez-de-chaussée |
Orateur | Pierre Ganty |
Email | pierreganty@gmail.com |
Url | UCLA, Los Angeles, California |
Aucun document lié à cet événement. RetourRetour à l'index
| |