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
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.

Abstract
Intelligent transportation systems (ITS) are gaining attraction in large cities for better traffic management. Traffic forecasting is an important part of ITS, but a difficult one due to the intricate spatiotemporal relationships of traffic between different locations. Despite the fact that remote or far sensors may have temporal and spatial similarities with the predicting sensor, existing traffic forecasting research focuses primarily on modeling correlations between neighboring sensors while disregarding correlations between remote sensors. Furthermore, existing methods for capturing spatial dependencies, such as graph convolutional networks (GCNs), are unable to capture the dynamic spatial dependence in traffic systems. Self-attention-based techniques for modeling dynamic correlations of all sensors currently in use overlook the hierarchical features of roads and have quadratic computational complexity. Our paper presents a new Dynamic Graph Convolution LSTM Network (DyGCN-LSTM) to address the aforementioned limitations. The novelty of DyGCN-LSTM is that it can model the underlying non-linear spatial and temporal correlations of remotely located sensors at the same time. Experimental investigations conducted using four real-world traffic data sets show that the suggested approach is superior to state-of-the-art benchmarks by 25% in terms of RMSE.

Abstract
Determining the relatedness of publications by detecting similarities and connections between researchers and their outputs can help science stakeholders worldwide to find areas of common interest and potential collaboration. To this end, many studies have tried to explore authorship attribution and research similarity detection through the use of automatic approaches. Nonetheless, inferring author research relatedness from imperfect data containing errors and multiple references to the same entities is a long-standing challenge. In a previous study, we conducted an experiment where a homogeneous crowd of volunteers contributed to a set of author name disambiguation tasks. The results demonstrated an overall accuracy higher than 75% and we also found important effects tied to the confidence level indicated by participants in correct answers. However, this study left many open questions regarding the comparative accuracy of a large heterogeneous crowd with monetary rewards involved. This paper seeks to address some of these unanswered questions by repeating the experiment with a crowd of 140 online paid workers recruited via MTurk's microtask crowdsourcing platform. Our replication study shows high accuracy for name disambiguation tasks based on authorship-level information and content features. These findings can be of greater informative value since they also explore hints of crowd behavior activity in terms of time duration and mean proportion of clicks per worker with implications for interface and interaction design.

Abstract