Cookies Policy
The website need some cookies and similar means to function. If you permit us, we will use those means to collect data on your visits for aggregated statistics to improve our service. Find out More
Accept Reject
  • Menu
Publications

2026

Specification-Guided Repair of Arithmetic Errors in Dafny Programs Using LLMs

Authors
Wu, V; Mendes, A; Abreu, A;

Publication
SOFTWARE ENGINEERING AND FORMAL METHODS, SEFM 2025

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 preconditions, 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 realworld 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.

2026

Optimizing Quay Crane Operations Considering Energy Consumption

Authors
de Almeida, JPR; Carrillo-Galvez, A; Morán, JP; Soares, TA; Mourao, ZS;

Publication
PROGRESS IN ARTIFICIAL INTELLIGENCE, EPIA 2025, PT II

Abstract
Seaport cranes operate continuously and consume large amounts of energy while aiming to minimise containerships' berthing time. Although previous studies have contributed to addressing the crane scheduling problem, most have focused exclusively on loading time, often overlooking the aspect of energy consumption. Furthermore, crane activity is typically modelled in a simplified manner-commonly assuming a fixed cycle duration or constant energy usage when handling a container-without accounting for the impact of variable container masses. In this study, an energy-aware quay crane scheduling formulation for container terminals is proposed, highlighting the importance of integrating an energy model into the scheduling problem. The optimisation problem is formulated as a Mixed Integer Linear Programming (MILP) model. The objective is to minimise total energy costs by reordering the sequence in which containers are handled, while respecting precedence constraints defined by the ship's stowage plan. Two solution methods-a MILP approach solved using CPLEX and a genetic algorithm (GA)-are compared. The results indicate that, for larger containerships, the genetic algorithm provides a more efficient solution method. Moreover, incorporating detailed energy consumption models for electric cranes may significantly reduce energy costs during containership handling operations.

2026

Tactical Overlay Interpretation: A Pattern-Recognition Study of Compact VLMs

Authors
Godinho, A; Figueira, A;

Publication
ICPRAM

Abstract

2026

Machine Learning-Based Cost Estimation Approach for Furniture Manufacturing

Authors
Pereira, T; Oliveira, EE; Amaral, A; Pereira, MG;

Publication
ADVANCES IN PRODUCTION MANAGEMENT SYSTEMS. CYBER-PHYSICAL-HUMAN PRODUCTION SYSTEMS: HUMAN-AI COLLABORATION AND BEYOND, APMS 2025, PT I

Abstract
This project was developed to improve the cost estimation process of new products within the Product Development Department of a furniture manufacturer. This work involved developing a methodology using Machine Learning (ML) models trained on products' existing data to predict the cost of new innovative ones based on similarities and given data. The ML models used were Linear Regression (LR), Light Gradient-Boosting Machine (LGBM), Random Forest (RF), and Support Vector Machine (SVM). The proposed methodology considers the estimation of the total cost of producing a product, which encompasses both material and operational costs. Throughout this project, several analyses were developed to identify and evaluate different independent variables that could explain the behaviour of these two cost components. The suitability of the different variables was studied by applying several ML models, and a set of functions that return an estimate of the cost as a function of these predictor variables was obtained. The proposed approach, which incorporates ML models into more complex variables to predict, resulted in a 19.29% reduction in estimation error.

2026

HUydra: Full-Range Lung CT Synthesis via Multiple HU Interval Generative Modelling

Authors
Cardoso, A; Sousa, P; Pereira, T; Oliveira, HP;

Publication
CoRR

Abstract

2026

A Conceptual Framework to Design Patterns of Horizontal Collaboration in Co-opetitive Logistics Partnerships

Authors
Carvalho, L; de Sousa, JF; de Sousa, JP;

Publication
HYBRID HUMAN-AI COLLABORATIVE NETWORKS, PRO-VE 2025, PT I

Abstract
Despite the recognised potential of horizontal collaboration in logistics to reduce inefficiencies, and the increasing academic interest in this topic, in practice many initiatives fail. One of the main reasons for this failure is the poor strategy planning and governance organisation. This paper addresses this gap proposing a comprehensive conceptual framework to support the design and implementation of a common strategy for the stakeholders of such partnerships. The research employs qualitative methods, drawing on interviews and the case analysis of existent initiatives. The proposed framework involves the main phases of the strategic formulation, deciding the stakeholder engagement, strategic formulation, operational implementation, and business model elaboration. It serves as a road map for stakeholders to avoid common mistakes and accelerate the deployment of cooperative partnerships.

  • 32
  • 4483