Abstract
The continuous evolution of programming languages has brought benefits and new challenges for software developers. In recent years, we have witnessed a rapid release of new versions of mainstream programming languages like Java. While these advancements promise better security, enhanced performance, and increased developers' productivity, the constant release of new language versions has posed a particular challenge for practitioners: how to keep their systems up-to-date with new language releases. This thesis aims to understand the pains, motivations, and practices developers follow during rejuvenating efforts-a particular kind of software maintenance whose goal is to avoid obsolesce due to the evolution of programming languages. To this end, we are building and validating a theory using a mixed methods study. In the first study, we interviewed 23 software developers and used the Constructivist Grounded Theory Method to identify recurrent challenges and practices used in rejuvenation efforts. In the second study, we mined the software repositories of open-source projects written in C++ and JavaScript to identify the adoption of new language features and whether or not software developers conduct large rejuvenation efforts. The first study highlights the benefits of new feature adoption and rejuvenation, revealing developer methods and challenges. The second study emphasizes open-source adoption trends and patterns for modern features. In the third and final study, our goal is to share our theory on software rejuvenation with practitioners through the Focus Group method with industrial patterns.

Abstract

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

Abstract
This document presents the case study for the ABZ 2023 conference. The case study introduces a safety critical interactive system called AMAN (Arrival MANager), which is a partly-autonomous scheduler of landing sequences of aircraft in airports. This interactive systems interleaves Air Traffic Controllers activities with automation in AMAN. While some AMAN systems are currently deployed in airports, we consider here only a subset of functions which represent a challenge in modelling and verification.

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.