FormaliSE 2024
Fri 12 - Sun 21 April 2024 Lisbon, Portugal
co-located with ICSE 2024
Mon 15 Apr 2024 14:30 - 15:00 at Eugénio de Andrade - Machine learning and formal methods Chair(s): Stefania Gnesi

This research idea paper proposes leveraging Large Language Models (LLMs) to enhance the productivity of Dafny developers. Although the use of verification-aware languages, such as Dafny, has increased considerably in the last decade, these are still not widely adopted. Often the cost of using such languages is too high, due to the level of expertise required from the developers and challenges that they often face when trying to prove a program correct. Even though Dafny automates a lot of the verification process, sometimes there are steps that are too complex for Dafny to perform on its own. One such case is that of missing lemmas, i.e. Dafny is unable to prove a result without being given further help in the form of a theorem that can assist it in the proof of the step.

In this paper, we describe preliminary work on a new Dafny plugin that leverages LLMs to assist developers by generating suggestions for relevant lemmas that Dafny is unable to discover and use. Moreover, for the lemmas that cannot be proved automatically, the plugin also attempts to provide accompanying calculational proofs. We also discuss ideas for future work by describing a research agenda on using LLMs to increase the adoption of verificationaware languages in general, by increasing developers productivity and by reducing the level of expertise required for crafting formal specifications and proving program properties.

Mon 15 Apr

Displayed time zone: Lisbon change

14:00 - 15:30
Machine learning and formal methodsFormaliSE 2024 at Eugénio de Andrade
Chair(s): Stefania Gnesi Istituto di Scienza e Tecnologie dell'Informazione "Alessandro Faedo"
14:00
30m
Talk
Case Study: Neural Network Malware Detection Verification for Feature and Image Datasets
FormaliSE 2024
Preston K. Robinette Vanderbilt University, Diego Manzanas Lopez Vanderbilt University, Serena Serbinowska Vanderbilt University, Kevin Leach Vanderbilt University, Taylor T Johnson Vanderbilt University
Pre-print
14:30
30m
Talk
Leveraging Large Language Models to Boost Dafny’s Developers Productivity
FormaliSE 2024
Álvaro F. Silva Independent Researcher, Alexandra Mendes University of Porto and HASLab, INESC TEC, João F. Ferreira INESC-ID and IST, University of Lisbon
15:00
10m
Day closing
Closing
FormaliSE 2024