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
Mobile acceptance testing remains a bottleneck in modern software development, particularly for cross-platform mobile development using frameworks like Flutter. While developers increasingly rely on automated testing tools, creating and maintaining acceptance test artifacts still demands significant manual effort. To help tackle this issue, we introduce AToMIC, an automated framework leveraging specialized Large Language Models to generate Gherkin scenarios, Page Objects, and executable UI test scripts directly from requirements (JIRA tickets) and recent code changes. Applied to BMW's MyBMW app, covering 13 real-world issues in a 170+ screen codebase, AToMIC produced executable test artifacts in under five minutes per feature on standard hardware. The generated artifacts were of high quality: 93.3% of Gherkin scenarios were syntactically correct upon generation, 78.8% of PageObjects ran without manual edits, and 100% of generated UI tests executed successfully. In a survey, all practitioners reported time savings (often a full developer-day per feature) and strong confidence in adopting the approach. These results confirm AToMIC as a scalable, practical solution for streamlining acceptance test creation and maintenance in industrial mobile projects.

Abstract

Abstract
The development of safety-critical systems is heavily governed by domain-specific standards. In the aerospace industry, the DO-178C-Software Considerations in Airborne Systems and Equipment Certification-serves as the primary certification standard used by agencies such as the FAA and EASA to review and approve software-based systems. Although DO-178C aims to ensure system safety while providing evidence for certification, it does not prescribe a specific software development process, allowing flexibility for traditional Waterfall, Agile, or hybrid methods with appropriate adaptations for the aerospace context. This study proposes Scrum4DO178C, an Agile process based on Scrum, to meet the demanding requirements of aerospace software, including safety, robustness, reliability, and integrity. Scrum4DO178C introduces novel process enhancements specifically tailored to meet these criticality needs, while aligning with the standard. Unlike previous proposals that lack detail, this research presents a comprehensive, validated process applied in a real-world industry project at the highest criticality level (Level A - Catastrophic), offering insights beyond theoretical scenarios. The findings demonstrated that the Scrum4DO178C process improves project performance, allows frequent and manageable requirement changes, reduces Verification & Validation (V&V) effort, and increases efficiency while maintaining full compliance with DO-178C. The study also identifies areas for further improvement and suggests exploring the process in additional case studies, both within the aerospace industry and other domains with similarly stringent safety-critical requirements. Finally, it confirms that appropriate automation, namely for documentation production, is a central element to further improve the process.

Abstract

Abstract