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 | |||
16:30 30mTalk | Desynchronized Multi-State Abstractions for Open Programs in Dynamic Languages ESOP Arlen Cox University of Colorado Boulder, Bor-Yuh Evan Chang University of Colorado Boulder, Xavier Rival INRIA/CNRS/ENS Paris | ||
17:00 30mTalk | Fine-grained Detection of Privilege Escalation Attacks on Browser Extensions ESOP Stefano Calzavara Università Ca' Foscari Venezia, Michele Bugliesi Università Ca' Foscari Venezia, Silvia Crafa University of Padova, Enrico Steffinlongo Università Ca' Foscari Venezia | ||
17:30 30mTalk | Analysis of Asynchronous Programs with Event-Based Synchronization ESOP Michael Emmi IMDEA Software Institute, Pierre Ganty IMDEA Software Institute, Rupak Majumdar MPI-SWS, Fernando Rosa-Velardo Universidad Complutense de Madrid |