The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
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.