Abstract

Abstract
The structure of a reactive transition system can to be modified on the fly by e.g. removing, reversing or adding new transitions. The topic has been studied by D. Gabbay and his collaborators in different contexts. In this paper we take their work a step further, introducing a suitable notion of bisimulation and obtaining a Hennessy-Milner theorem with respect to a hybrid logic in which transition properties can be expressed. Our motivation is to provide a characterisation of equivalence for such systems in order to exploit their possible roles in the formal description of software connectors in Reo, either from a behavioural (semantic) or spatial (syntactic) point of view.

Abstract
The analysis of sentiments, emotions, and opinions in texts is increasingly important in the current digital world. The existing lexicons with emotional annotations for the Portuguese language are oriented to polarities, classifying words as positive, negative, or neutral. To identify the emotional load intended by the author, it is necessary to also categorize the emotions expressed by individual words. EmoSpell is an extension of a morphological analyzer with semantic annotations of the emotional value of words. It uses Jspell as the morphological analyzer and a new dictionary with emotional annotations. This dictionary incorporates the lexical base EMOTAIX. PT, which classifies words based on three different levels of emotions-global, specific, and intermediate. This paper describes the generation of the EmoSpell dictionary using three sources: the Jspell Portuguese dictionary and the lexical bases EMOTAIX. PT and SentiLex-PT. Additionally, this paper details the Web application and Web service that exploit this dictionary. It also presents a validation of the proposed approach using a corpus of student texts with different emotional loads. The validation compares the analyses provided by EmoSpell with the mentioned emotional lexical bases on the ability to recognize emotional words and extract the dominant emotion from a text.

Abstract
We give a language-based security treatment of domain-specific languages and compilers for secure multi-party computation, a cryptographic paradigm that. enables collaborative computation over encrypted data. Computations are specified in a core imperative language, as if they were intended to be executed by a trusted-third party, and formally verified against. an information-flow policy modelling (an upper bound to) their leakage. This allows non-experts to assess the impact of performance driven authorized disclosure of intermediate values. Specifications are then compiled to multi-party protocols. We formalize protocol security using (distributed) probabilistic information-flow and prove security-preserving compilation: protocols only leak what. is allowed by the source policy. The proof exploits a natural but previously missing correspondence between simulation-based cryptographic proofs and (composable) probabilistic non-interference. Finally, we extend our framework to justify leakage cancelling, a domain-specific optimization that allows to first write an efficient specification that fails to meet the allowed leakage upper-bound, and then apply a probabilistic preprocessing that brings leakage to the acceptable range.

Abstract
The purpose of this study was to measure the subject's sense of presence while they performed a task (riding a bicycle downhill) in a virtual reality (VR) environment and to compare it by body position (standing vs. sitting) and gender. The sample consisted of 35 subjects (19 male and 16 female) between 17 and 33 years of age. A translated and validated Portuguese version of the lgroup Presence Questionnaire (IPQp) and the Reflexive Motor Acts (RMAs), based on direct observation, were used as metrics. The results showed significant differences between body position at the level of Experienced Realism, Spatial Presence and Overall Sense of Presence. When measuring RMAs, it was demonstrated that people in the sitting position presented a higher frequency. We concluded that body position influences perceptions of credibility, which has an impact on the sense of presence. No differences were identified between the genders.

Abstract
This paper presents LRMalloc, a lock-free memory allocator that leverages lessons of modern memory allocators and combines them with a lock-free scheme. Current state-of-the-art memory allocators possess good performance but lack desirable lock-free properties, such as, priority inversion tolerance, kill-tolerance availability, and/or deadlock and livelock immunity. LRMalloc’s purpose is to show the feasibility of lock-free memory management algorithms, without sacrificing competitiveness in comparison to commonly used state-of-the-art memory allocators, especially for concurrent multithreaded applications. © 2019, Springer Nature Switzerland AG.