Abstract
Alloy is a lightweight formal method that is well suited to teaching logic because it combines expressive logics with automatic analysis and visual feedback. In this paper, we report our experience using specification challenges on the Alloy4Fun platform in our formal methods courses. We briefly describe the types of challenges we have used over the years and discuss how different hints can help students make progress in solving them. Our main conclusion is that specification challenges are highly engaging and useful for students, but they should be balanced with broader modeling and validation activities to support long-term learning outcomes. They are also useful for research, because Alloy4Fun's datacollection infrastructure enables the release of open datasets that can be mined for insights into Alloy usage and for the evaluation of new tools and techniques.

Abstract

Abstract
Abstract Background Cognitive behavioral therapy (CBT) is an effective and widely used treatment for major depressive disorder (MDD). However, access is limited by long waiting lists and a shortage of trained therapists. Evidence-based guided and self-guided digital interventions can address these challenges, but their large-scale adoption in routine primary and specialized mental health care has been slow. Blended CBT (bCBT), combining face-to-face therapy with structured, guided digital treatment modules, may increase treatment capacity while maintaining the benefits of therapist support. Objective The European Comparative Effectiveness Research on Internet-based Depression Treatment study, conducted across 9 European countries, is the first large-scale comparative bCBT study for MDD. The hypothesis was that bCBT is clinically noninferior and cost-effective when compared with treatment as usual (TAU), which mainly consisted of face-to-face CBT. Methods A multisite randomized controlled trial was conducted with a noninferiority margin of d =0.20. Main inclusion criteria were age =18 years, a diagnosis of MDD based on the Mini International Neuropsychiatric Interview, and a baseline Patient Health Questionnaire-9 (PHQ-9) score of =5. The primary outcome was the PHQ-9, with secondary outcomes including MDD remission at 12 months, therapeutic alliance, and costs. Intention-to-treat analyses were performed, and linear mixed modeling was used to assess intervention effects. Cost-effectiveness analyses were conducted from a health care perspective. Results A total of 835 patients were included in the study. bCBT was shown to be noninferior to TAU on the primary PHQ-9 outcome during treatment (3 months after the baseline assessment, d =-0.26, 95% CI -0.43 to -0.09), at 6 months (posttreatment, d =-0.21, 95% CI -0.39 to-0.04), and at 12-month follow-up ( d =-0.01, 95% CI -0.19 to 0.17). Furthermore, the bCBT group had a significantly lower likelihood of experiencing an MDD episode at 12 months (odds ratio 0.67, 95% CI 0.45-0.99). Subgroup analyses indicated that participants with and with no antidepressant use at baseline in both groups benefited equally from their treatment. Deterioration rates (Reliable Change Index) were below 5% in both groups. bCBT appeared acceptable for patients and therapists, with a strong working alliance in both groups. From a health care perspective, bCBT was not cost-effective at 12 months' assessment, as its total costs were not significantly lower than TAU. However, the probability that bCBT is cost-effective is high (0.95) at a willingness to pay (WTP) of €3800 per improvement in the PHQ-9 score, and 0.76 at a WTP of €10,000 per MDD case prevented (average 2017 exchange rate was €1=US $1.13). Conclusions bCBT offers an effective and safe digitally supported alternative to face-to-face TAU for patients with MDD and their therapists in routine clinical care. From a health care perspective, its cost-effectiveness depends on policymakers’ WTP for the additional clinical benefits achieved.

Abstract
Early fault detection remains a critical challenge in predictive maintenance (PdM), particularly within critical infrastructure, where undetected failures or delayed interventions can compromise safety and disrupt operations. Traditional anomaly detection methods are typically reactive, relying on real-time sensor data to identify deviations as they occur. This reactive nature often provides insufficient lead time for effective maintenance planning. To address this limitation, we propose a novel two-stage early detection framework that integrates time series forecasting with anomaly detection to anticipate equipment failures several hours in advance. In the first stage, future sensor signal values are predicted using forecasting models; in the second, conventional anomaly detection algorithms are applied directly to the forecasted data. By shifting from real-time to anticipatory detection, the framework aims to deliver actionable early warnings, enabling timely and preventive maintenance. We validate this approach through a case study focused on metro train systems, an environment where early fault detection is crucial for minimizing service disruptions, optimizing maintenance schedules, and ensuring passenger safety. The framework is evaluated across three forecast horizons (1, 3, and 6 hours ahead) using twelve state-of-the-art anomaly detection algorithms from diverse methodological families. Detection performance is assessed using five performance metrics. Results show that anomaly detection remains highly effective at short to medium horizons, with performance at 1-hour and 3-hour forecasts comparable to that of real-time data. Ensemble and deep learning models exhibit strong robustness to forecast uncertainty, maintaining consistent results with real-time data even at 6-hour forecasts. In contrast, distance- and density-based models suffer substantial degradation at longer horizons (6-hours), reflecting their sensitivity to distributional shifts in predicted signals. Overall, the proposed framework offers a practical and extensible solution for enhancing traditional PdM systems with proactive capabilities. By enabling early anomaly detection on forecasted data, it supports improved decision-making, operational resilience, and maintenance planning in industrial environments.

Abstract

Abstract
Generative artificial intelligence (GenAI) promises substantial productivity gains for organisations, yet unresolved questions about data management and privacy continue to shape managers' and employees' confidence. This study examines workplace adoption of GenAI and shows how trust, conditioned by perceptions of data-management integrity, information transparency, and privacy risk, influences acceptance. This mixed-method study tests, using a survey-based structural equation model plus interviews focused on managerial practices among daily GenAI practitioners, two core insights: (i) trust is the strongest predictor of intention to use GenAI, and (ii) trust depends chiefly on manager's and employees' belief that organisational data are handled reliably and objectively through management routines. Perceptions of transparency or privacy risk exert no direct influence on either trust or usage. Building on these results, the study delineates four managerial domains: data-management process, information transparency, privacy risk, and trust, alongside twenty future research questions designed to understand how GenAI is linked to managerial practices. For practice, the findings recommend monitoring, calibrated disclosure, and adaptive privacy protocols as concrete managerial levers to strengthen GenAI acceptance. The evidence highlights trustworthy data governance, not abstract explainability, as the foundation of sustainable GenAI adoption. The study also provides a roadmap of actionable management practices to guide its implementation in modern workplaces.