Abstract
Data collection is pervasively bound to our digital lifestyle. A recent study reports that the growth of the data created and replicated in 2020 was even higher than in the previous years to an astonishing global amount of 64.2 zettabytes of data. There are numerous companies whose services/products rely heavily on data analysis, and mining the produced data has already revealed great value for businesses in different sectors. In order to be able to support the professionals that do this job, typically known as data scientists, we first need to characterize them. To contribute towards this characterization, we conducted a public survey and in this work we present the results about a particular aspects of their life: the tools they use and need. © 2022 IEEE Computer Society. All rights reserved.

Abstract

Abstract
Team automata describe networks of automata with input and output actions, extended with synchronisation policies guiding how many interacting components can synchronise on a shared input/output action. Given such a team automaton, we can reason over communication properties such as receptiveness (sent messages must be received) and responsiveness (pending receives must be satisfied). Previous work focused on how to identify these communication properties. However, automatically verifying these properties is non-trivial, as it may involve traversing networks of interacting automata with large state spaces. This paper investigates (1) how to characterise communication properties for team automata (and subsumed models) using test-free propositional dynamic logic, and (2) how to use this characterisation to verify communication properties by model checking. A prototype tool supports the theory, using a transformation to interact with the mCRL2 tool for model checking. © 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.

Abstract
Pulp and Paper Companies collaborate to monitor and monetize waste and create value from their by-products. This process of Industrial Symbiosis requires the creation and maintenance of trusted and transparent relationships between all entities participating in these networks, which is a constant challenge. In this context, a blockchain-based system can help in establishing and maintaining these networks, serving as a ground truth between companies operating at a national or a global scale. This paper proposes a scalable and modular blockchain architecture design using smart contracts to enhance the industrial symbiosis process of the Pulp, Paper, and Cardboard Production Sector companies in Portugal. This design comprehends all entities participating in the network. The implementation of this design assumes the use of a permissioned ledger built using Hyperledger Fabric to provide the required trust and transparency between all entities.

Abstract
Programs with a continuous state space or that interact with physical processes often require notions of equivalence going beyond the standard binary setting in which equivalence either holds or does not hold. In this paper we explore the idea of equivalence taking values in a quantale V, which covers the cases of (in)equations and (ultra)metric equations among others. Our main result is the introduction of a V-equational deductive system for linear ?-calculus together with a proof that it is sound and complete (in fact, an internal language) for a class of enriched autonomous categories. In the case of inequations, we get an internal language for autonomous categories enriched over partial orders. In the case of (ultra)metric equations, we get an internal language for autonomous categories enriched over (ultra)metric spaces. We use our results to obtain examples of inequational and metric equational systems for higher-order programs that contain real-time and probabilistic behaviour.

Abstract
The complexity of the number of stakeholders, information systems used, and port operations evoke new challenges to port security when it comes to the total knowledge and control of the overall operations of transport and parking of containerized freight, namely hazmat ones. The rising interest and the port authorities' awareness of the relevance of security concerns involved in this complex ecosystem has led to the search for new technological solutions that allow, in an integrated manner, the smart and automatic control of operations of transport and hazardous freight parking in all the areas of its jurisdiction, without third-party dependencies. Despite its importance and criticality, port authorities tend to have limited real-time knowledge of the location of hazmat containers, whether moving within the port (entering and leaving), or in its parking, having a direct impact on the port security. This article presents a Digital Twin platform for 3D and real-time georeferenced visualization of container parks and the location of hazardous containerized freight. This tool combines different modules that further allow to visualize information associated to a container, its movement, as well as its surrounding area, including a realistic and dynamic 3D representation of what is the area encircling the port.