Abstract
Pulse oximeters are medical devices used to assess peripheral arterial oxygen saturation (SpO(2)) noninvasively. In contrast, the gold standard requires arterial blood to be drawn to measure the arterial oxygen saturation (SaO(2)). Devices currently on the market measure SpO(2) with lower accuracy in populations with darker skin tones. Pulse oximetry inaccuracies can yield episodes of hidden hypoxemia (HH), with SpO(2) >= 88%, but SaO(2) < 88%. HH can result in less treatment and increased mortality. Despite being flawed, pulse oximeters remain ubiquitously used; debiasing models could alleviate the downstream repercussions of HH. To our knowledge, this is the first study to propose such models. Experiments were conducted using the MIMIC-IV dataset. The cohort includes patients admitted to the Intensive Care Unit with paired (SaO(2), SpO(2)) measurements captured within 10min of each other. We built a XGBoost regression predicting SaO(2) from SpO(2), patient demographics, physiological data, and treatment information. We used an asymmetric mean squared error as the loss function to minimize falsely elevated predicted values. The model achieved R-2 = 67.6% among Black patients; frequency of HH episodes was partially mitigated. Respiratory function was most predictive of SaO(2); race-ethnicity was not a top predictor. This singlecenter study shows that SpO(2) corrections can be achieved with Machine Learning. In future, model validation will be performed on additional patient cohorts featuring diverse settings.

Abstract
When crowd workers provide their contributions in a shared working environment, they may be influenced by the inputs of other contributors in implicit ways. Stigmergy in crowdsourcing consists of tracking changes in work activities to guide crowd workers based on the digital traces left by other workers. In such scenarios, there is no direct communication between the contributors. Still, the traceable changes they left during their actions act as a mediating element that clearly affects the final work product. From a behavior analysis perspective, the properties recorded in event logs can be of practical value in observing the behavioral traces produced by crowd workers when performing microtasks. This form of task fingerprinting has been explored for over a decade to better understand performance-related data and user navigational behavior in crowdsourcing markets. In line with this, the goal of this paper is to study the feasibility of task fingerprinting alongside the stigmergic effect occurring in a crowdsourcing setting through a user event logger. To this end, a case study was conducted using a real-world scenario of extreme weather phenomena represented on interactive maps. Each user could observe the traces of other crowd members while providing annotations. Twelve experts in weather forecasting were recruited to participate in this study to annotate extreme weather events. The results indicate that it is possible to use task fingerprinting for tracking the stigmergic effect in such activities with gains in terms of implicit coordination. Furthermore, the task fingerprinting allowed to map participants with similar behavioral traces, suggesting an increase in the accuracy of annotation clusters.

Abstract
This paper presents a proof system for reasoning about execution time bounds for a core imperative programming language. Proof systems are defined for three different scenarios: approximations of the worst-case execution time, exact time reasoning, and less pessimistic execution time estimation using amortized analysis. We define a Hoare logic for the three cases and prove its soundness with respect to an annotated cost-aware operational semantics. Finally, we define a verification conditions (VC) generator that generates the goals needed to prove program correctness, cost, and termination. Those goals are then sent to the Easycrypt toolset for validation. The practicality of the proof system is demonstrated with an implementation in OCaml of the different modules needed to apply it to example programs. Our case studies are motivated by real-time and cryptographic software.

Abstract
Sectorization consists of grouping the basic units of a large territory to deal with a complex problem involving different criteria. Resectorization rearranges a current sectorization avoiding substantial changes, given a set of conditions. The paper considers the case of the distribution of geographic areas of fire brigades in the north of Portugal so that they can protect and rescue the population surrounding the fire stations. Starting from a current sectorization, assuming the geographic and population characteristics of the areas and the fire brigades’ response capacity, we provide an optimized resectorization considering two objectives: to reduce the rescue time by maximizing the compactness criterion, and to avoid overload situations by maximizing the equilibrium criterion. The solution method is based on the Non-dominated Sorting Genetic Algorithm (NSGA-II). Finally, computational results are presented and discussed. © 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.

Abstract
AbstractWe advance Mixmash-AIS, a multimodal optimization music mashup creation model for loop recombination at scale. Our motivation is to (1) tackle current scalability limitations in state-of-the-art (brute force) computational mashup models while enforcing the (2) compatibility of audio loops and (3) a pool of diverse mashups that can accommodate user preferences. To this end, we adopt the artificial immune system (AIS) opt-aiNet algorithm to efficiently compute a population of compatible and diverse music mashups from loop recombinations. Optimal mashups result from local minima in a feature space representing harmonic, rhythmic, and spectral musical audio compatibility. We objectively assess the compatibility, diversity, and computational performance of Mixmash-AIS generated mashups compared to a standard genetic algorithm (GA) and a brute force (BF) approach. Furthermore, we conducted a perceptual test to validate the objective evaluation function within Mixmash-AIS in capturing user enjoyment of the computer-generated loop mashups. Our results show that while the GA stands as the most efficient algorithm, the AIS opt-aiNet outperforms both the GA and BF approaches in terms of compatibility and diversity. Our listening test has shown that Mixmash-AIS objective evaluation function significantly captures the perceptual compatibility of loop mashups (p < .001).

Abstract
This second workshop on HCI Engineering Education aims at carrying forward work on identifying, examining, structuring, and sharing educational resources and approaches to support the process of teaching/learning Human-Computer Interaction (HCI) Engineering. The widening range of available interaction technologies and their applications in increasingly varied contexts (private or professional) underlines the importance of teaching HCI Engineering but also the difficulty of taking into account changes and developments in this field in often static university curricula. Besides, as these technologies are taught in diverse curricula (ranging from Human Factors and Psychology to hardcore Computer Science), we are interested in what the best approaches and best practices are to integrate HCI Engineering topics in the curricula of programs in Software Engineering, Computer Science, Human-computer Interaction, Psychology, Design, etc. The workshop is proposed on behalf of the IFIP Working Group 2.7/13.4 on User Interface Engineering.