Abstract
Safety-critical interactive systems pose design and evaluation challenges that go beyond usability. The safety of the system (i.e. the guarantee that it does not reach an undesirable or incorrect state) is also a relevant consideration. Traditional user-centred approaches (UCD) lack the rigour and thoroughness needed to address safety, and formal verification arises as a possible solution. Applying formal verification to a safety-critical interactive system design encompasses developing a model, expressing and verifying properties, and analysing the verification results. In the case of model checking, properties are typically expressed in temporal logic. This creates a gap between the languages used in UCD and the languages used for formal verification. Creating temporal logic properties manually requires expertise in formal methods and can be both time-consuming and error-prone. This paper explores how a patterns-based approach can be used to support the specification of properties in a natural language-based style. A prototype implementation of the approach is evaluated through a user study, and the results of this evaluation are discussed.

Abstract
A key feature of model finding techniques allows users to enumerate and explore alternative solutions. However, it is challenging to guarantee that the generated instances are relevant to the user, representing effectively different scenarios. This challenge is exacerbated in quantitative modelling, where one must consider both the qualitative, structural part of a model, and the quantitative data on top of it. This results in a search space of possibly infinite candidate solutions, often infinitesimally similar to one another. Thus, research on instance enumeration in qualitative model finding is not directly applicable to the quantitative context, which requires more sophisticated methods to navigate the solution space effectively. The main goal of this paper is to explore a generic approach for navigating quantitative solution spaces and showcase different iteration operations, aiming to generate instances that differ considerably from those previously seen and promote a larger coverage of the search space. Such operations are implemented in QAlloy - a quantitative extension to Alloy - on top of Max-SMT solvers, and are evaluated against several examples ranging, in particular, over the integer and fuzzy domains.

Abstract
The staggered model is a recent, very general variant of discrete-time quantum walks which, avoiding the use of a coin to direct the walker evolution, explores the underlying graph structure to build an evolution operator based on local unitaries induced by adjacent vertices. Optimising their implementation to increase resilience to decoherence phenomena motivates their analysis with the ZX-calculus. The whole optimisation can be seen as a graph reconfiguration process along which the original circuit is rewrote, significantly reducing the number of (expensive) gates used. The exercise identified an underlying pattern leading to an alternative, potentially more efficient evolution operator.

Abstract
This paper introduces Paraconsistent Reactive Graphs, as an extension of Reactive graphs that incorporates paraconsistency into the ground edges to address vagueness and inconsistency within dynamic systems. By assigning pairs of truth values to ground edges, this framework captures the uncertainty and contradictions stemming from incomplete or conflicting information. We explore the semantics of these graphs and provide a practical example to illustrate the proposed approach.

Abstract

Abstract
Breakthroughs in sequencing technologies led to an exponential growth of genomic data, providing novel biological insights and therapeutic applications. However, analyzing large amounts of sensitive data raises key data privacy concerns, specifically when the information is outsourced to untrusted third-party infrastructures for data storage and processing (e.g., cloud computing). We introduce Gyosa, a secure and privacy-preserving distributed genomic analysis solution. By leveraging trusted execution environments (TEEs), Gyosa allows users to confidentially delegate their GWAS analysis to untrusted infrastructures. Gyosa implements a computation partitioning scheme that reduces the computation done inside the TEEs while safeguarding the users' genomic data privacy. By integrating this security scheme in Glow, Gyosa provides a secure and distributed environment that facilitates diverse GWAS studies. The experimental evaluation validates the applicability and scalability of Gyosa, reinforcing its ability to provide enhanced security guarantees.