A visit by Sergio Mover

Looking forward to hosting a visit by Sergio Mover, who will give a talk on “Lifestate: Event-Driven Protocols and Callback Control Flow” at 10:30 on Thursday, 5th of September, in the Inria Lille Building B seminar room.

Abstract: Developing interactive applications (apps) against event-driven software frameworks such as Android is notoriously difficult. To create apps that behave as expected, developers must follow complex and often implicit asynchronous programming protocols. Such protocols intertwine the proper registering of callbacks to receive control from the framework with appropriate application-programming interface (API) calls that in turn affect the set of possible future callbacks. An app violates the protocol when, for example, it calls a particular API method in a state of the framework where such a call is invalid.

What makes automated reasoning hard in this domain is largely what makes programming apps against such frameworks hard: the specification of the protocol is unclear, and the control flow is complex, asynchronous, and higher-order.

In this talk, we tackle the problem of specifying and modeling event-driven application-programming protocols. We first formalize a core meta-model capturing the dialogue between event-driven frameworks and application callbacks. Based on this meta-model, we define a language called lifestate that permits precise and formal descriptions of application-programming protocols and the callback control flow imposed by the event-driven framework. Lifestate unifies modeling what app callbacks can expect of the framework with specifying rules the app must respect when calling into the framework. In this way, we effectively combine lifecycle constraints and typestate rules.

We provide a dynamic verification algorithm that takes as input a trace of execution of an app and a lifestate protocol specification to either produce a trace witnessing a protocol violation or a proof that no such trace is realizable.

We evaluate our approach experimentally, showing that lifestate modeling is “sufficient and necessary“, and that it’s rigorous formalization avoids model unsoundness, differently from existing framework models.

Short bio: Sergio Mover is an assistant professor at Ecole Polytechnique. His main research focuses on the development of theory and tools to automatically reason about Cyber-Physical systems and software, and more recently in applying machine learning and data mining techniques to learn software properties from existing code bases. Sergio obtained a Ph.D. degree in 2014 from the University of Trento and Fondazione Bruno Kessler, Italy. Sergio was then a postdoctoral researcher in the Computer Science Department at the University of Colorado Boulder, and is a faculty member at Ecole Polytechnique since October 2018.

With financial support by the Hauts-de-France region