01whole.pdf (622.33 kB)
Download file

Applying automatic program verification techniques to spreadsheets

Download (622.33 kB)
thesis
posted on 28.03.2022, 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.

History

Table of Contents

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

Notes

Empirical thesis. Bibliography: pages 59-65

Awarding Institution

Macquarie University

Degree Type

Thesis MRes

Degree

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

Department, Centre or School

Department of Computing

Year of Award

2019

Principal Supervisor

Anthony Sloane

Rights

Copyright Sarah Heimlich 2019. Copyright disclaimer: http://mq.edu.au/library/copyright

Language

English

Extent

1 online resource (vxiii, 65 pages) diagrams

Former Identifiers

mq:71123 http://hdl.handle.net/1959.14/1271094