ESOP 2015
Tue 14 - Thu 16 April 2015 London, United Kingdom
Tue 14 Apr 2015 11:00 - 11:30 at Skeel - Session 1 Chair(s): Jan Vitek

Spreadsheets are widely used, yet are error-prone: they use a weak type system, allowing certain operations that will silently return unexpected results, like comparisons of integer values with string values. However, discovering these issues is hard, since data and formulas can be dynamically set, read or modified. We propose a static analysis that detects all run-time type-unsafe operations in spreadsheets. It is based on an abstract interpretation of spreadsheet applications, including spreadsheet tables, global re-evaluation and associated programs. Our implementation supports the features commonly found in real-world spreadsheets. We ran our analyzer on the EUSES Spreadsheet Corpus. This evaluation shows that our tool is able to automatically verify a large number of real spreadsheets, runs in a reasonable time and discovers complex bugs that are difficult to detect by code review or by testing.

Tue 14 Apr

Displayed time zone: Azores change

10:30 - 12:30
Session 1ESOP at Skeel
Chair(s): Jan Vitek Northeastern University
10:30
30m
Talk
Probabilistic Programs as Spreadsheet Queries
ESOP
Andrew D. Gordon Microsoft Research and University of Edinburgh, Claudio Russo Microsoft Research, Marcin Szymczak University of Edinburgh, Johannes Borgström Uppsala University, Nicolas Rolland Microsoft Research, Thore Graepel Microsoft Research, Daniel Tarlow Microsoft Research
11:00
30m
Talk
Static Analysis of Spreadsheet Applications for Type-Unsafe Operations Detection
ESOP
Tie Cheng CNRS, ENS, INRIA, Paris, France, Xavier Rival INRIA/CNRS/ENS Paris
11:30
30m
Talk
Running Probabilistic Programs Backwards
ESOP
Neil Toronto Brigham Young University, Jay McCarthy , David Van Horn
12:00
30m
Talk
A Verified Compiler for Probability Density Functions
ESOP
Manuel Eberl Technische Universität München, Johannes Hölzl Technische Universität München, Tobias Nipkow Technische Universität München