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
[No abstract available]

Abstract

Abstract

Abstract
The rapid growth of data traffic and evolving service demands are driving a shift from traditional network architectures to advanced solutions. While 5G networks provide reduced latency and higher availability, they still face limitations due to reliance on integrated hardware, leading to configuration and interoperability challenges. The emerging Open Radio Access Network (O-RAN) paradigm addresses these issues by enabling remote configuration and management of virtualized components through open interfaces, promoting cost-effective, multi-vendor interoperability. Network slicing, a key 5G enabler, allows for tailored network configurations to meet heterogeneous performance requirements. The main contribution of this paper is a private Standalone 5G network based on O-RAN, featuring a dynamic Data Radio Bearer Management xApp (xDRBM) for real-time metric collection and traffic prioritization. xDRBM optimizes resource usage and ensures performance guarantees for specific applications. Validation was conducted in an emulated environment representative of real-world scenarios. © ICST Institute for Computer Sciences, Social Informatics and Telecommunications Engineering 2025.

Abstract