SAS 2023
Sun 22 - Tue 24 October 2023 Cascais, Portugal
co-located with SPLASH 2023
Sun 22 Oct 2023 09:05 - 10:05 at Room I - Session 1 Chair(s): Caterina Urban

Static analysis is typically about computing a global over-approxi- mation of a program’s behavior from its source code. But what if most of the program code is missing or unknown to the analyzer? What if even where the program starts is unknown? This fundamentally thorny situation arises when attempting to analyze interactive applications (apps) developed against modern, event-driven software frameworks. Rich event-driven software frameworks enable software engineers to create complex applications on sophisticated computing platforms (e.g., smartphones with a broad range of sensors and rich interactivity) with relatively little code by simply implementing callbacks to respond to events. But developing apps against them is also notoriously difficult. To create apps that behave as expected, devel- opers must follow the complex and opaque asynchronous programming protocols imposed by the framework. So what makes static analysis of apps hard is essen- tially what makes programming them hard: the specification of the programming protocol is unclear and the possible control flow between callbacks is largely un- known. While the typical workaround to perform static analysis with an unknown framework implementation is to either assume it to be arbitrary or attempt to eagerly specify all possible callback control flow, this solution can be too pes- simistic to prove properties of interest or too burdensome and tricky to get right. In this talk, I argue for a rethinking of how to analyze app code in the context of an unknown framework implementation. In particular, I present some benefits from taking a goal-directed or backward-from-error formulation to prove just the assertions of interest and from designing semantics, program logics, specification logics, and abstract domains to reason about the app-framework boundary in a first-class manner. What follows are hopefully lines of work that make ana- lyzing modern interactive applications more targeted, more compositional, and ultimately more trustworthy.

Sun 22 Oct

Displayed time zone: Lisbon change

09:00 - 10:30
Session 1SAS 2023 at Room I
Chair(s): Caterina Urban Inria & École Normale Supérieure | Université PSL
SAS 2023
Manuel Hermenegildo Technical University of Madrid (UPM) and IMDEA Software Institute, José Morales IMDEA Software Institute
Goal-Directed Abstract Interpretation and Event-Driven FrameworksKeynote
SAS 2023
I: Bor-Yuh Evan Chang University of Colorado at Boulder; Amazon
A Product of Shape and Sequence Abstractions (Radhia Cousot Young Researcher Best Paper Award)
SAS 2023
Josselin Giet Ecole Normale Supérieure, Félix Ridoux Univ Rennes / IMDEA Software Institute, Xavier Rival Inria; ENS; CNRS; PSL University