Authors
Simon Ausserlechner, Sandra Fruhmann, Wolfgang Wieser, Birgit Hofer, Raphael Spork, Clemens Muhlbacher, & Franz Wotawa
Abstract
Spreadsheets are undoubtedly the most prominent example of end-user programs vastly used in practice. Spreadsheets are often complex and comprise several hundreds or even thousands of formulas making fault localization a very hard and painstaking task.
Although there has been work based on model-based reasoning for fault localization in spreadsheets, its applicability in practice is still limited mainly due to two reasons. First, most of the available constraint solvers, used for computing diagnoses, do not sufficiently support Real numbers. Second, the runtime especially for larger spreadsheets is too long preventing truly interactive debugging.
In order to eliminate limitations regarding data type support and runtime performance, we suggest the use of SMT solvers for spreadsheet debugging. Besides lying out the foundations of SMT solving for diagnoses, we introduce its application to spreadsheet debugging.
The empirical evaluation shows that the SMT solver Z3 requires six times less time for computing diagnoses compared to public available constraint solvers.
Sample
In this example, cell B7 contains a wrong value. Model-based software debugging (MBSD) helps to identify the possible root causes, which leads to the formula error in cell B4.
Publication
2013, International Conference on Quality Software, July, pages 139-148
Full article
The right choice matters! SMT solving substantially improves model-based debugging of spreadsheets
