An Abstract Domain to Infer Types over Zones in Spreadsheets
Abstract
Spreadsheet languages are very commonly used, by large user
bases, yet they are error prone. However, many semantic issues and errors
could be avoided by enforcing a stricter type discipline. As declaring and
specifying type information would represent a prohibitive amount of work
for users, we propose an abstract interpretation based static analysis for
spreadsheet programs that infers type constraints over zones of spreadsheets, viewed as two-dimensional arrays. Our abstract domain consists
in a cardinal power from a numerical abstraction describing zones in a
spreadsheet to an abstraction of cell values, including type properties.
We formalize this abstract domain and its operators (transfer functions,
join, widening and reduction) as well as a static analysis for a simplified spreadsheet language. Last, we propose a representation for abstract
values and present an implementation of our analysis.
Keywords
Abstract domain, Spreadsheet, Array analysis, Abstract interpretation, Verificatioin, Static Analysis.