Write a Blog >>
SPLASH 2017
Sun 22 - Fri 27 October 2017 Vancouver, Canada
Thu 26 Oct 2017 15:30 - 15:52 at Regency C - Verification in Practice Chair(s): Davide Ancona

In JavaScript programs, asynchrony arises in situations such as web-based user-interfaces, communicating with servers through HTTP requests, and non-blocking I/O. Event-based programming is the most popular approach for managing asynchrony, but suffers from problems such as lost events and event races, and results in code that is hard to understand and debug. Recently, ECMAScript 6 has added support for promises, an alternative mechanism for managing asynchrony that enables programmers to chain asynchronous computations while supporting proper error handling. However, JavaScript promises are complex and error-prone in their own right, so programmers would benefit from techniques that can reason about the correctness of promise-based code.   Since the ECMAScript 6 specification is informal and intended for implementors of JavaScript engines, it does not provide a suitable basis for formal reasoning. This paper presents lambda_P, a core calculus that captures the essence of EcmaScript 6 promises. Based on lambda_P, we introduce the promise graph, a program representation that can assist programmers with the debugging of promise-based code. We then report on a case study in which we investigate how the promise graph can be helpful for debugging errors in promise-based code fragments reported on the StackOverflow forum. As another application of lambda_P, we systematically derive a static analysis that can be used to compute an over-approximation of the promise graph.

Thu 26 Oct

splash-2017-OOPSLA
15:30 - 17:00: OOPSLA - Verification in Practice at Regency C
Chair(s): Davide Ancona
splash-2017-OOPSLA150902460000015:30 - 15:52
Talk
DOI
splash-2017-OOPSLA150902595000015:52 - 16:15
Talk
DOI
splash-2017-OOPSLA150902730000016:15 - 16:37
Talk
DOI
splash-2017-OOPSLA150902865000016:37 - 17:00
Talk
DOI