Abstract
Data analysis has emerged as a cornerstone in facilitating informed decision-making across myriad fields, in particular in software development and project management. This integrative practice proves instrumental in enhancing operational efficiency, cutting expenditures, mitigating potential risks, and delivering superior results, all while sustaining structured organization and robust control. This paper presents ITC, a synergistic platform architected to streamline multi-organizational and multi-workspace collaboration for project management and technical documentation. ITC serves as a powerful tool, equipping users with the capability to swiftly establish and manage workspaces and documentation, thereby fostering the derivation of invaluable insights pivotal to both technical and business-oriented decisions. ITC boasts a plethora of features, from support for a diverse range of technologies and languages, synchronization of data, and customizable templates to reusable libraries and task automation, including data extraction, validation, and document automation. This paper also delves into the predictive analytics aspect of the ITC platform. It demonstrates how ITC harnesses predictive data models, such as Random Forest Regression, to anticipate project outcomes and risks, enhancing decision-making in project management. This feature plays a critical role in the strategic allocation of resources, optimizing project timelines, and promoting overall project success. In an effort to substantiate the efficacy and usability of ITC, we have also incorporated the results and feedback garnered from a comprehensive user assessment conducted in 2022. The feedback suggests promising potential for the platform's application, setting the stage for further development and refinement. The insights provided in this paper not only underline the successful implementation of the ITC platform but also shed light on the transformative impact of predictive analytics in information systems.

Abstract
Strategic term re-writing and attribute grammars are two powerful programming techniques widely used in language engineering. The former relies on strategies to apply term re-write rules in defining large-scale language transformations, while the latter is suitable to express context-dependent language processing algorithms. These two techniques can be expressed and combined via a powerful navigation abstraction: generic zippers. This results in a concise zipper-based embedding offering the expressiveness of both techniques. Such elegant embedding has a severe limitation since it recomputes attribute values. This paper presents a proper and efficient embedding of both techniques. First, attribute values are memoized in the zipper data structure, thus avoiding their re-computation. Moreover, strategic zipper based functions are adapted to access such memoized values. We have implemented our memoized embedding as the Ztrategic library and we benchmarked it against the state-of-the-art Strafunski and Kiama libraries. Our first results show that we are competitive against those two well established libraries.

Abstract
In this paper we present the first formally verified implementations of Kyber and, to the best of our knowledge, the first such implementations of any post-quantum cryptosystem. We give a (readable) formal specification of Kyber in the EasyCrypt proof assistant, which is syntactically very close to the pseudocode description of the scheme as given in the most recent version of the NIST submission. We present high-assurance open-source implementations of Kyber written in the Jasmin language, along with machine-checked proofs that they are functionally correct with respect to the EasyCrypt specification. We describe a number of improvements to the EasyCrypt and Jasmin frameworks that were needed for this implementation and verification effort, and we present detailed benchmarks of our implementations, showing that our code achieves performance close to existing hand-optimized implementations in C and assembly.

Abstract
Slight variations in user interface response times can significantly impact the user experience provided by an interface. Load testing is used to evaluate how an application behaves under increasing loads. For interactive applications, load testing can be done by directly calling services at the business logic or through the user interface. In modern web applications, there is a considerable amount of control logic on the browser side. The impact of this logic on applications' behaviour is only fully considered if the tests are done through the user interface. Capture reply tools are used for this, but their use can become costly. Leveraging an existing model-based testing tool, we propose an approach to automate load testing done through the user interface.

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
The IVY workbench is a model-based tool for the formal modelling and verification of interactive systems. The tool uses model checking to carry out the verification step. The goal is not to replace, but to complement more exploratory and iterative user-centred design approaches. However, the need for formal and rigorous modelling and reasoning raises challenges for the integration of both approaches. This paper presents a new plugin that aims to provide support for the integration of the formal methods based analysis supported by the tool, with user-centred design. The plugin is described, and an initial validation of its functionalities presented.