Abstract
The interaction of light with matter in near-to-resonant conditions opens a path for the exploration of nontrivial optical response that can play an important role in future photonics-driven technology. But as the attention shifts towards many-level atomic systems and involving multi-dimensional experimental scenarios, the complexity of the physical systems makes the analytical approach to the semiclassical model of the MaxwellBloch equations impossible without any strongly-limiting approximations. In this context, robust and highperformance computational tools are mandatory. In this work, we describe the development and implementation of a cross-platform Maxwell-Bloch numerical solver that is capable to exploit the different hardware available to tackle efficiently the problems under consideration. Moreover, it is demonstrated that this simulation tool can address a vast class of problems with considerable reduction of simulation time, featuring speedups up to 30 when running in massive parallel GPUs compared with the same codes running on a CPU, showing its potential towards addressing a large class of modern problems in photonics.

Abstract
We present a machine-checked proof of security for the domain management protocol of Amazon Web Services' KMS (Key Management Service) a critical security service used throughout AWS and by AWS customers. Domain management is at the core of AWS KMS; it governs the top-level keys that anchor the security of encryption services at AWS. We show that the protocol securely implements an ideal distributed encryption mechanism under standard cryptographic assumptions. The proof is machine-checked in the EasyCrypt proof assistant and is the largest EasyCrypt development to date.

Abstract
Rapidly changing customer demands, regulations and technologies drive the complexity of products, processes and production systems, as well as shorter product and factory lifecycles. In order to handle such complexity while decreasing the time-to-market, immersive virtual reality (VR) technologies are increasingly being used in industry to support product and factory lifecycle engineering processes, such as (re)design, validation and verification, learning and training. However, the design and development of multi-user VR training for complex and manual production processes remain a challenge for industry. The integration of VR training simulations with virtual and physical factories could support the handling of such obstacles in terms of efficiency and effectiveness by increasing the precision, accuracy and reliability of data used in VR simulations. In this study, we present a collaborative and coordinated VR training model and its data integration with virtual factory tools and manufacturing execution systems for a wind turbine assembly scenario. A demonstration has been performed and evaluated by industry experts. The preliminary evaluation results show that integrated collaborative VR training has significant potential for more efficient and effective training, as well as enabling new use cases for industry.

Abstract
The energy requirements of thruster driven autonomous underwater vehicle (AUV) missions have been growing in recent years. Their complexity and length are continuously increasing due to the growth of undersea exploration. The use of variable buoyancy systems (VBS) can potentially lead to energy savings since consumption is only required for buoyancy changes. As such, energy is only spent during limited periods of time, as opposed to thruster driven systems, where consumption is typically continuous. In this work, an energetic comparison between thruster and VBS driven devices is performed for a specific mission profile and a defined set of parameters. The influence of the mission parameters is studied in order to determine which system leads to the lowest energy consumption. For the case study presented, it is shown that the use of VBS over thrusters can lead to considerable energetic savings. © 2019 IEEE.

Abstract
We propose (formula presented) -logic as a formal foundation for the specification and development of event-based systems with local data states. The logic is intended to cover a broad range of abstraction levels from abstract requirements specifications up to constructive specifications. Our logic uses diamond and box modalities over structured actions adopted from dynamic logic. Atomic actions are pairs where e is an event and (formula presented) a state transition predicate capturing the allowed reactions to the event. To write concrete specifications of recursive process structures we integrate (control) state variables and binders of hybrid logic. The semantic interpretation relies on event/data transition systems; specification refinement is defined by model class inclusion. For the presentation of constructive specifications we propose operational event/data specifications allowing for familiar, diagrammatic representations by state transition graphs. We show that (formula presented) -logic is powerful enough to characterise the semantics of an operational specification by a single (formula presented) -sentence. Thus the whole development process can rely on (formula presented) -logic and its semantics as a common basis. This includes also a variety of implementation constructors to support, among others, event refinement and parallel composition. © The Author(s) 2019.

Abstract
This paper proposes the implementation of a framework for the development of collaborative extended reality (XR) applications. Using the framework, developers can focus on understanding which collaborative mechanisms they need to implement for the respective reality model application. In this paper we specifically study collaborative mechanisms around object manipulation in Virtual Reality (VR). As such, we planned a VR prototype using the proposed framework, which was used to validate the various interaction and collaboration features in VR. The gathered data from the user tests revealed that they enjoyed the experience and the collaborative mechanisms helped them work together. Furthermore, to understand whether the framework allowed for the development of XR applications, we decided to implement an augmented reality prototype as well. Afterwards, we ran an experiment with 4 VR and 3 AR users sharing the same virtual environment. The experiment was successful at allowing them to interact in real-time in the same shared environment. Therefore, the framework enables the development of XR applications that support different mixed-reality technologies.