In this work, we propose a formal model of asynchronous event-driven programs which goes a long way in bridging the semantic gap between programs and existing models, in particular by allowing the dynamic creation of concurrent tasks, events, task buffers, and threads, and capturing precisely the interaction between these quantities. We demonstrate that the analogous program analysis problems based on our new model remain decidable, and that our new model is strictly more expressive than the existing Petri net based models. Our proof relies on a class of high-level Petri nets called Data Nets, whose tokens carry names taken from an infinite and linearly ordered domain. This result represents a significant expansion to the decidability frontier for concurrent program analyses.
Wed 15 AprDisplayed time zone: Azores change
16:30 - 18:00
|Desynchronized Multi-State Abstractions for Open Programs in Dynamic Languages|
|Fine-grained Detection of Privilege Escalation Attacks on Browser Extensions|
|Analysis of Asynchronous Programs with Event-Based Synchronization|