Abstract
This special issue showcases state-of-the-art research at the intersection of analytics and retail operations. As the retail landscape becomes increasingly complex - driven by omnichannel strategies, evolving customer expectations, and a surge in data availability - analytics has emerged as a critical enabler of operational efficiency, customer experience, responsiveness, and sustainability and ethics. Collectively, these contributions demonstrate how advanced analytics can support retailers in navigating uncertainty, personalizing services, and scaling up innovation across formats and channels. The articles featured in this issue address a diverse set of decision domains, including warehousing, inventory and assortment planning, and distribution and last-mile delivery. Methodologically, they span descriptive, prescriptive, and hybrid approaches, leveraging tools such as machine learning, stochastic modeling, and dynamic optimization. By grounding models in real-world data and focusing on practical implementation, the issue provides actionable insights for both scholars and practitioners. It also highlights emerging opportunities for future research on behavioral integration, human-machine collaboration, and the ethical dimensions of retail analytics.

Abstract
In this paper, we introduce a novel approach for rigorously verifying safety properties of state machine specifications. Our method leverages an auto-active verifier and centers around the use of action functions annotated with contracts. These contracts facilitate inductive invariant checking, ensuring correctness during system execution. Our approach is further supported by the Why3-do library, which extends the Why3 tool's capabilities to verify concurrent and distributed algorithms using state machines. Two distinctive features of Why3-do are: (i) it supports specification refinement through refinement mappings, enabling hierarchical reasoning about distributed algorithms; and (ii) it can be easily extended to make verifying specific classes of systems more convenient. In particular, the library contains models allowing for message-passing algorithms to be described with programmed handlers, assuming different network semantics. A gallery of examples, all verified with Why3 using SMT solvers as proof tools, is also described in the paper. It contains several auto-actively verified concurrent and distributed algorithms, including the Paxos consensus algorithm.

Abstract
Purpose - This study proposes a conceptual framework for strategic sourcing tailored to Project Management Offices (PMOs) operating in complex Research, Development and Innovation (R&D&I) environments, examining how R&D&I PMOs orchestrate sourcing by identifying key elements and practices that define this strategic role. Design/methodology/approach - This study uses a qualitative approach grounded in a three-year ethnographic immersion within a military scientific, technological and innovation institution. Data collection involved participant observation, document analysis and informal interviews, enabling an in-depth examination of sourcing dynamics. Findings - The resulting framework integrates three interdependent pillars: five foundational sourcing dimensions; a strategic make-or-buy decision matrix; and management categories aligned with R&D&I operations. The findings show that PMOs coordinate strategic sourcing by integrating internal and external capabilities, thereby enhancing organizational responsiveness in complex innovation ecosystems. Research limitations/implications - While the single-case ethnographic study focuses on the aerospace and defense sector, the framework distinguishes between general conceptual pillars and context-specific applications, supporting its conceptual transferability to other highly regulated sectors such as healthcare and pharmaceuticals. The study provides actionable guidance for managing technological uncertainty and power dynamics, while addressing economic, political and teaching implications. Practical implications - The proposed framework offers PMO managers a strategic sourcing model suited to complex environments such as the defense sector. It strengthens decision-making by making make-or-buy tradeoffs explicit, documented and comparable across technology acquisition, capability development, outsourcing boundaries and interinstitutional partnerships under confidentiality and intellectual property constraints. The model addresses recurring problems in R&D&I settings, including fragmented criteria, inconsistent rationales and limited traceability, enhancing transparency, governance and alignment with organizational goals. It positions the PMO as a strategic actor in acquisition and technological alliance decisions, offering guidance for institutional adaptation, particularly relevant for public organizations facing budgetary and regulatory constraints. Social implications - The societal implications of this study stem from the role of the R&D&I PMO as a catalyst for technological sovereignty and national development. By structuring strategic sourcing in highly complex environments, the proposed model strengthens the national technological and industrial base, reduces dependence on external critical technologies and enhances innovation capacity. The findings show that dual-use R&D projects generate positive spillovers for industry and academia, fostering regional development and national competitiveness. By coordinating government, industry and research institutions through the Triple Helix, the PMO helps ensure that R&D&I investments translate into tangible socioeconomic benefits for society. Originality/value - This research addresses the underexplored intersection of strategic sourcing, project management and innovation governance. It goes beyond theoretical abstraction by providing a model for navigating technological uncertainty. It explores how emerging digital technologies (such as Artificial Intelligence and blockchain) can refine decision-making and support the automation of Intellectual Property safeguards.

Abstract
The rapid expansion of solar photovoltaic (SPV) systems poses critical challenges to material supply security and waste management. Addressing these challenges require integrating circular economy strategies. This study develops a dynamic and probabilistic material flow analysis (MFA) to quantify the lifecycle material flows of crystalline silicon (c-Si) modules from 1998 to 2050, with waste projections extended to 2099. Three circular economy scenarios are evaluated, integrating the European Union Directive targets and strategies for reducing, reusing, and recycling. Uncertainty is explicitly addressed through Monte Carlo simulation, capturing variability in installed capacity projections, Weibull lifetime parameters, material composition, pre-operational losses, and recycling efficiencies. Portugal is used as a national-scale case study to demonstrate the applicability of the proposed methodology. Results indicate a cumulative material requirement of approximately 1.46 Mt by 2050 without circular strategies. Across low-, medium-, and high-circularity scenarios, both total material demand and the share of primary versus secondary raw materials vary substantially. Notably, scenarios incorporating reuse may increase primary material extraction due to reduced availability of secondary materials for manufacturing. Deterministic analysis suggests that full c-Si loop closure can be achieved between 2039 and 2041, depending on the scenario. However, probabilistic results reveal substantial uncertainty, with the probability of 100% Circular Material Use Rate (CMUR) in the period 2030-2050 among 53.7%, 43.6% and 68.6% under low, medium, and high circularity respectively. Sensitivity analysis identifies future c-Si's deployment and lifetimes as the dominant drivers of circularity outcomes. This probabilistic MFA contributes with robust evidence to support circular economy policy design and infrastructure planning while opening avenues for further research.

Abstract
Ambient intelligence (AmI) refers to environments where smart devices, sensors, and AI-driven systems work seamlessly to enhance human interactions with their surroundings. Through the combination of real-time data, context-awareness, and adaptive learning, AmI enables environments to respond proactively to user needs, improving efficiency, comfort, and decision-making. However, since AmI systems are inherently human-centric and often operate autonomously, they must be designed with robust ethical, privacy, and safety considerations. Ensuring that these systems function reliably, fairly, and without harm is crucial, especially in sensitive domains like healthcare, security, and smart infrastructure. This work introduces a novel tool, conceptualized as an AmI Digital Twin, which allows developers to simulate or monitor AmI data streams, and develop and thoroughly test AmI applications before and during their real use. Built on a modular architecture leveraging technologies like React.js, Node.js, Kafka, Faust, MongoDB, InfluxDB, Grafana, and Docker, the platform ensures adaptability to different application environments, scalability, and ease of deployment. Besides the description of the tool itself, we provide some early validation results in common AmI tasks such as anomaly and concept drift detection. The tool is available in a public repository, and comes pre-packaged with a set of applications for AmI use-cases. © The Author(s), under exclusive license to Springer Nature Switzerland AG 2026.

Abstract