Cookies Policy
The website need some cookies and similar means to function. If you permit us, we will use those means to collect data on your visits for aggregated statistics to improve our service. Find out More
Accept Reject
  • Menu
Research Opportunity
Apply now Final Selection Minute View Formal Call
Research Opportunity

Formal Methods


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


Cluster / Centre

Computer Science / High-Assurance Software

Scientific Advisor

José Nuno Oliveira