ABSTRACT. We propose a framework for expressing and analyzing the Quality of Service (QoS) of message-passing systems using a choreographic model that consists of g-choreography and Communicating Finite State machines (CFSMs).

Our framework relies on three technical contributions: (I) We propose an extension of CFSMs with quantitative non-functional contracts that express costs or values associated with local computations. (II) We define a dynamic temporal logic capable of expressing QoS properties of systems relative to the g-choreography that specifies the communication protocol. (III) We prove that the logic is semi-decidable and leverage its semi-decision procedure to define a bounded model-checking approach to verify whether a system of CFSMs satisfies a QoS property or not.

ABSTRACT. Matching logic (ML) is a formalism for specifying and reasoning about mathematical structures by means of patterns and pattern matching. Previously, it has been used to capture a number of other logics, e.g., separation logic with recursive definitions and linear temporal logic. ML has also been formalized in the Coq Proof Assistant, and the soundness of its Hilbert-style proof system has been mechanized.

However, using a Hilbert-style system for interactive reasoning is challenging - even more so in ML, which lacks a general deduction theorem. Therefore, we propose a single-conclusion sequent calculus for ML that is more amenable to interactive proving. Based on this sequent calculus, we implement a proof mode for interactive reasoning in ML, which significantly simplifies the construction of ML proofs in Coq. The proof mode is a mechanism for displaying intermediate proof states and an extensible set of proof tactics that implement the rules of the sequent calculus. We evaluate our proof mode on a collection of examples, showing a substantial improvement in proof script size and readability.

ABSTRACT. Nowadays, the main advances in computational power are due to parallelism. However, most parallel languages have been designed with a focus on processors and threads. This makes dealing with data and memory in programs hard, which distances the implementation from its original algorithm. We propose a new paradigm for parallel programming, the data-autonomous paradigm, where computation is performed by autonomous data elements. Programs in this paradigm are focused on making the data collaborate in a highly parallel fashion. We furthermore present AuDaLa, the first data autonomous programming language, and include an operational semantics. Programming in AuDaLa is very natural, as illustrated by examples, albeit in a style very different from sequential and contemporary parallel programming.

ABSTRACT. The increased complexity of high-integrity digital systems designs with intricate interactions between numerous components has placed a greater need on ensuring that the design satisfies its intended requirements. This digital assurance can only come about through rigorous mathematical analysis of the design. This manuscript provides a detailed description of the formal language semantics used for modeling and verification of systems. Models are developed using Event-B by building on a formalised semantics that enables the constructions of triggered enable statecharts with a run-to-completion scheduling. Rodin has been used to develop and analyse models using this semantics.

ABSTRACT. This paper provides foundations for strong (that is, possibly under abstraction) call-by-value evaluation for the lambda-calculus. Recently, Accattoli et al. proposed a form of call-by-value strong evaluation for the lambda-calculus, the external strategy, and proved it reasonable for time. Here, we study the external strategy using a semantical tool, namely Ehrhard's call-by-value multi types, a variant of intersection types. We show that the external strategy terminates exactly when a term is typable with so-called shrinking multi types, mimicking similar results for strong call-by-name. Additionally, the external strategy is normalizing in the untyped setting, that is, it reaches the normal form whenever it exists.

We also consider the call-by-extended-value approach to strong evaluation introduced by Grégoire and Leroy, and recently shown reasonable for time by Biernacka et al. The two approaches turn out to *not* be equivalent: there are terms that are externally divergent but terminating for call-by-extended-value.

ABSTRACT. The intersection non-emptiness problem of regular languages is one of the most classical and fundamental decision problems in formal language theory, which plays an important role in many areas. Because of its wide applications, the efficiency of the algorithms becomes particularly crucial. In practice, it is quite common that automata have large numbers of states, therefore the explicit construction of automata may incur significant costs in terms of both time and space, significantly impacting the performance of the related programs. To overcome this challenge, in this paper, we present four efficient algorithms for checking the intersection of regular expressions without the need for automata construction. Our algorithms employ lazy evaluation strategies to simulate intersection non-emptiness checking on automata to avoid constructing automata. They also use automata with fewer states to reduce the state complexity. We conducted experiments and compared our results with six state-of-the-art SMT solvers. The results show significant advantages of our algorithms over existing methods, achieving significant speedups over the current SMT solvers.

ABSTRACT. We consider global models of communicating agents specified as transition systems labelled by interactions in which multiple senders and receivers can participate. A realisation of such a model is a set of local transition systems—one for each agent—which are executed concurrently using synchronous communication. Our core challenge is how to check whether a global model is realisable and, if it is, how to synthesise a realisation. We identify and compare two variants to realise global interaction models, both relying on bisimulation equivalence. Then we investigate, for both variants, realisability conditions to be checked on global models. We propose a synthesis method for the construction of realisations by grouping locally indistinguishable states. The paper is accompanied by a tool that implements realisability checks and synthesises realisations.

ABSTRACT. Developing critical components, such as mission controllers or embedded systems, is a challenging task. Reactive synthesis is a technique to automatically produce correct controllers. Given a high-level specification written in LTL, reactive synthesis consists of computing a system that satisfies the specification as long as the environment respects the assumptions. Unfortunately, LTL synthesis suffers from high computational complexity which precludes its use for many large cases. A promising approach to improve synthesis scalability consists of decomposing a safety specification into smaller specifications, that can be processed independently and composed into a solution for the original specification. Previous decomposition methods focus on identifying independent parts of the specification whose systems are combined via simultaneous execution. In this work, we propose a novel decomposition algorithm based on modes, which consists of decomposing a complex safety specification into smaller problems whose solution is then composed sequentially (instead of simultaneously). The input to our algorithm is the original specification and the description of the modes. We show how to generate sub-specifications automatically and we prove that if all sub-problems are realizable then the full specification is realizable. Moreover, we show how to construct a system for the original specification from sub-systems for the decomposed specifications. We finally illustrate the feasibility of our approach with multiple case studies using off-the-self synthesis tools to process the obtained sub-problems.