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
The U-Net is one of the most fundamental architectural advancements in the deep learning era. It is a crucial tool for image segmentation, especially for biomedical modalities. The research community seems to interpret the effectiveness of neural architectural search (such as the nn-U-Net) as evidence that architectural enhancements proposed since its debut are mostly unnecessary. We argue that there are still network-in-network primitives that can be leveraged to further enhance its performance, focusing on the squeeze-and-excitation (SE) pathway specifically in this paper. Specifically, we study its use of global descriptors, since it should be at odds with the spatial resolution required for dense-prediction tasks. It is theorized in the literature that performance is probably gained from some implicit ability of the learned excitations to filter supposedly uninformative channels during training. We explain this almost unreasonable success through an analysis of the empirical estimates of the excitation covariance matrix. Our analysis also directly contradicts the above conjecture - the most effective SE approach actually displayed the less extreme filtering behaviour, weighing all channels much closer to the mean (0.5). Our experiments are conducted in three diverse, staple biomedical modalities: dermoscopy, colonoscopy, and ultrasound. © 2025 European Signal Processing Conference, EUSIPCO. All rights reserved.

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