Alexandra Mendes, a researcher at INESC TEC, received the Amazon Research Award in automated reasoning. This is the first time this award has been granted to researchers who carry out their R&D work in Portugal.
The INESC TEC researcher won the prize with the project “Overcoming Barriers to the Adoption of Verification-Aware Languages”, which aims to identify and overcome the main obstacles to the adoption of programming languages with support for formal verification, with a particular focus on the Dafny language.
“The goal is to improve the usability of said languages and promote their integration into software development, fostering wider adoption of formal verification tools among programmers,” explained Alexandra Mendes.
The project will be developed in collaboration with Amazon Web Services (AWS), which will help bring academic research closer to the real needs of the industry. The support provided by this award includes funding and computational resources, enhancing the research capacity of INESC TEC in high-assurance software.
The proposal stems from the researcher’s experience in using, teaching, and developing formal verification tools, such as Dafny, Verus, and Why3. Although these languages show potential, they continue to present significant barriers to adoption outside highly specialised contexts.
“This study aims to provide a more systematic basis for identifying new priority features that support the adoption of these languages, helping to guide our efforts – and those of other research teams – more effectively,” she emphasised.
The project also seeks to address the lack of systematic studies documenting the challenges faced by potential users of these languages, thus contributing to the advancement of knowledge in the field.
In the long term, the results of this research could help create more robust and secure software, not only in critical contexts but also in everyday applications.
“If programming languages with formal verification support become more accessible to programmers in general, it could lead to greater adoption of these tools and, consequently, the production of more reliable software – not just in critical software contexts but also in everyday applications,” concluded the researcher.
The project will be developed as part of the collaboration between INESC TEC, the Faculty of Engineering of the University of Porto (FEUP), and Amazon Web Services.
The researcher mentioned in this news piece is associated with INESC TEC, the Faculty of Engineering of the University of Porto (FEUP) and the Software Reliability Lab, which she co-leads.
News, current topics, curiosities and so much more about INESC TEC and its community!
