Formal Methods
[Closed]
Work description
Spreadsheet tools, like Excel, are used massively by companies and other institutions in their decision making processes. Every spreadsheet program may start small and simple, but over time and through different users its quality degrades. Despite the impressive number of features available in spreadsheet software, the development tools is far less than optimal, making them unreliable and error prone. This project should investigate a new technique to formalize spreadsheet semantics based on typed linear algebra (LA). This theory should be used to capture both the syntax and semantics of spreadsheets, including spreadsheet usual operations (eg. sumproduct, running totals etc). The work should find inspiration in previous research in the field, including a LA approach to data cubes and the use the strongly typed linear algebra library in Haskell laop developed in a previous project to encode such formal spreadsheet models, paving the way to spreadsheet safety analysis and re-factoring. Besides the formal semantics definition, the project is expected to deliver tools for spreadsheet synthesis from LA specifications and a LA- semantics analyser for spreadsheets. This grant proposal is intended to fill this gap, which is regarded as a research opportunity for a Master Student in Informatics.
Academic Qualifications
Master's student in computer engineering or computer science.
Minimum profile required
Master's student in computer engineering or computer science that includes courses on formal methods.
Preference factors
Solid background in formal methods, relational algebra and linear algebra.
Application Period
Since 02 Mar 2022 to 15 Mar 2022
[Closed]
Cluster / Centre
Computer Science / High-Assurance Software