Macquarie University
01whole.pdf (622.33 kB)

Applying automatic program verification techniques to spreadsheets

Download (622.33 kB)
posted on 2022-03-28, 17:40 authored by Sarah Heimlich
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.


Table of Contents

1. Introduction -- 2. Background -- 3. Design considerations -- 4. The system -- 5. Results -- 6. Conclusions and future research -- Appendices.


Empirical thesis. Bibliography: pages 59-65

Awarding Institution

Macquarie University

Degree Type

Thesis MRes


MRes, Macquarie University, Faculty of Science and Engineering, Department of Computing

Department, Centre or School

Department of Computing

Year of Award


Principal Supervisor

Anthony Sloane


Copyright Sarah Heimlich 2019. Copyright disclaimer:




1 online resource (vxiii, 65 pages) diagrams

Former Identifiers