Abstract
Password managers (PMs) are important tools that enable the use of stronger passwords, freeing users from the cognitive burden of remembering them. Despite this, there are still many users who do not fully trust PMs. In this paper, we focus on a feature that most PMs offer that might impact the user's trust, which is the process of generating a random password. We present three of the most commonly used algorithms and we propose a solution for a formally verified reference implementation of a password generation algorithm. We use EasyCrypt to specify and verify our reference implementation. In addition, we present a proof-of-concept prototype that extends Bitwarden to only generate compliant passwords, solving a frequent users' frustration with PMs. This demonstrates that our formally verified component can be integrated into an existing (and widely used) PM.

Abstract
When developing mobile applications, developers often have to decide when to acquire and when to release resources. This leads to resource leaks, a kind of bug where a resource is acquired but never released. This is a common problem in Android applications that can degrade energy efficiency and, in some cases, can cause resources to not function properly. In this paper, we present an extension of EcoAndroid, an Android Studio plugin that improves the energy efficiency of Android applications, with an inter-procedural static analysis that detects resource leaks. Our analysis is implemented using Soot, FlowDroid, and Heros, which provide a static-analysis environment capable of processing Android applications and performing inter-procedural analysis with the IFDS framework. It currently supports the detection of leaks related to four Android resources: Cursor, SQLite-Database, Wakelock, and Camera. We evaluated our tool with the DroidLeaks benchmark and compared it with 8 other resource leak detectors. We obtained a precision of 72.5% and a recall of 83.2%. Our tool was able to uncover 191 previously unidentified leaks in this benchmark. These results show that our analysis can help developers identify resource leaks.

Abstract
The evolving landscape of software development demands that software testers continuously adapt to new tools, practices, and acquire new skills. This study investigates software testing competency needs in industry, identifies knowledge gaps in current testing education, and highlights competencies and gaps not addressed in academic literature. This is done by conducting two focus group sessions and interviews with professionals across diverse domains, including railway industry, healthcare, and software consulting and performing a curated small-scale scoping review. The study instrument, co-designed by members of the ENACTEST project consortium, was developed collaboratively and refined through multiple iterations to ensure comprehensive coverage of industry needs and educational gaps. In particular, by performing a thematic qualitative analysis, we report our findings and observations regarding: professional training methods, challenges in offering training in industry, different ways of evaluating the quality of training, identified knowledge gaps with respect to academic education and industry needs, future needs and trends in testing education, and knowledge transfer methods within companies. Finally, the scoping review results confirm knowledge gaps in areas such as AI testing, security testing and soft skills. © The Author(s), under exclusive license to Springer Nature Switzerland AG 2026.

Abstract
Context: Software testing is a critical aspect of the software development lifecycle, yet it remains underrepresented in academic curricula. Despite advances in pedagogical practices and increased attention from the academic community, challenges persist in effectively teaching software testing. Understanding these challenges from the teachers’ perspective is crucial to aligning education with industry needs. Objective: To analyze the characteristics, practices, tools, and challenges of software testing courses in higher education, from the perspective of educators, and to assess the integration of recent pedagogical approaches in software testing education. Method: A structured survey consisting of 52 questions was distributed to 143 software testing educators across Western European universities, resulting in 49 valid responses. The survey explored topics taught, course organization, teaching practices, tools and materials used, gamification approaches, and teacher satisfaction. Results: The survey revealed significant variability in course content, structure, and teaching methods. Most dedicated software testing courses are offered at the master’s level and are elective, whereas testing is introduced earlier in less specialized (NST) courses. There is low adoption of formal guidelines (e.g., ACM, SWEBOK), limited integration of non-functional testing types, and a high diversity in textbooks and tools used. While modern practices like Test-Driven Development and automated assessment are increasingly adopted, gamification and active learning approaches remain underutilized. Teachers expressed a need for improved and more consistent teaching materials. Conclusion: The study highlights a mismatch between academic practices and industry expectations in software testing education. Greater integration of standardized curricula, broader adoption of modern teaching tools, and increased support for teachers through high-quality, adaptable teaching materials are needed to enhance the effectiveness of software testing education.

Abstract
Debugging and repairing faults when programs fail to formally verify can be complex and time-consuming. Automated Program Repair (APR) can ease this burden by automatically identifying and fixing faults. However, traditional APR techniques often rely on test suites for validation, but these may not capture all possible scenarios. In contrast, formal specifications provide strong correctness criteria, enabling more effective automated repair. In this paper, we present an APR tool for Dafny, a verification-aware programming language that uses formal specifications — including pre-conditions, post-conditions, and invariants — as oracles for fault localization and repair. Assuming the correctness of the specifications and focusing on arithmetic bugs, we localize faults through a series of steps, which include using Hoare logic to determine the state of each statement within the program, and applying Large Language Models (LLMs) to synthesize candidate fixes. The models considered are GPT-4o mini, Llama 3, Mistral 7B, and Llemma 7B. We evaluate our approach using DafnyBench, a benchmark of real-world Dafny programs. Our tool achieves 89.7% fault localization success rate and GPT-4o mini yields the highest repair success rate of 74.18%. These results highlight the potential of combining formal reasoning with LLM-based program synthesis for automated program repair. © The Author(s), under exclusive license to Springer Nature Switzerland AG 2026.

Abstract