Applying automatic program verification techniques to spreadsheets

Errors in spreadsheets cost the global economy billions of dollars every year. Spreadsheets are a Turing complete functional end-user programming language. As such, it is not surprising that researchers have investigated how spreadsheet errors can be minimised and resolved using traditional software engineering practices. Despite general success in this field of research, spreadsheets exhibit many unique features that can make standard software engineering techniques difficult. In particular,as we will show, spreadsheets are a partially ordered, non-recursive class of programming languages that support native, automatic type conversion. We further spreadsheet research by proposing and creating a spreadsheet static analyser that automatically verifies whether a spreadsheet will execute without errors over a variety of inputs. The system statically analyses a program to locate spreadsheet specific errors then translates the spreadsheet into C so existing trace abstraction refinement verification tools can be used for common verification challenges. Using the tool, we analyze several spreadsheet corpora to determine the tool's efficacy.The tool was able to correctly determine the validity of all spreadsheets tested, find an undetected type system error, and determine lines of C code generated are a likely indicator of spreadsheet quality.