Abstract

Abstract
Recent verification tools aim to make formal verification more accessible for software engineers by automating most of the verification process. However, the manual work and expertise required to write verification helper code, such as loop invariants and auxiliary lemmas and assertions, remains a barrier. This paper explores the use of Large Language Models (LLMs) to automate the generation of loop invariants for programs in Dafny. We tested the approach on a curated dataset of 100 programs in Dafny involving arrays, strings, and numeric types. Using a multimodel approach that combines GPT-4o and Claude 3.5 Sonnet, correct loop invariants (passing the Dafny verifier) were generated at the first attempt for 92% of the programs, and in at most five attempts for 95% of the programs. Additionally, we developed an extension to the Dafny plugin for Visual Studio Code to incorporate automatic loop invariant generation into the IDE. Our work stands out from related approaches by handling a broader class of problems and offering IDE integration.

Abstract

Abstract

Abstract

Abstract
For the past fourteen years, the Workshop on Automating Test Case Design, Selection and Evaluation (A-TEST)1 has provided a venue for researchers and industry members alike to exchange and discuss trending views, ideas, state-of-the-art, work-in-progress, and scientific results on automated testing. The previous thirteen editions of A-TEST were co-located with several conferences over time: CISTI2 (first two editions), FEDCSIS 3 (three editions), and ESEC/FSE4 (seven editions). The 14th edition took place on September 15, 2023, in Kirchberg, Luxembourg, co-located with ASE 2023 (38th IEEE/ACM International Conference on Automated Software Engineering5). The A-TEST 2023 program featured an enlightening keynote on quantum software testing, followed by three technical sessions in which the authors of 6 full papers and 4 short papers dived into various aspects of automated testing, from neuroevolution and fuzzing techniques to GUI-based software testing and test case recommendations. This short report summarizes the keynote and paper presentations at A-TEST 2023.