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

Displayed time zone: Tijuana, Baja California change

15:30 - 17:00
Verification in PracticeOOPSLA at Regency C
Chair(s): Davide Ancona University of Genova
15:30
22m
Talk
A Model for Reasoning about JavaScript Promises
OOPSLA
Magnus Madsen University of Waterloo, Ondřej Lhoták University of Waterloo, Canada, Frank Tip Northeastern University
DOI
15:52
22m
Talk
Robust and Compositional Verification of Object Capability Patterns
OOPSLA
David Swasey MPI-SWS, Germany, Deepak Garg Max Planck Institute for Software Systems, Derek Dreyer MPI-SWS
DOI
16:15
22m
Talk
A Verified Messaging System
OOPSLA
William Mansky Princeton University, Andrew W. Appel Princeton, Aleksey Nogin HRL Laboratories, LLC
DOI
16:37
22m
Talk
Who Guards the Guards? Formal Validation of the ARM v8-M Architecture Specification
OOPSLA
DOI