Abstract
With the incresasing importance of program verification, an issue that has been receiving more attention is the certification of verification tools, addressing the vernacular question: Who verifies the verifier?. In this paper we approach this meta-verification problem by focusing on a fundamental component of program verifiers: the Verification Conditions Generator (VCGen), responsible for producing a set of proof obligations from a program and a specification. The semantic foundations of VCGens lie in program logics, such as Hoare logic, Dynamic logic, or Separation logic, and related predicate transformers. Dynamic logic is the basis of the KeY system, one of the foremost deductive verifiers, whose logic makes use of the notion of update, which is quite intricate to formalize. In this paper we derive systematically, based on a KeY-style dynamic logic, a correct-by-construction VCGen for a toy programming language. Our workflow covers the entire process, from the logic to the VCGen. It is implemented in the Why3 tool, which is itself a program verifier. We prove the soundness and (an appropriate notion of) completeness of the logic, then define a VCGen for our language and establish its soundness. Dynamic logic is one of a variety of research topics that our dear friend and colleague Luis Soares Barbosa has, over the years, initiated and promoted at the University of Minho. It is a pleasure for us to dedicate this work to him on the occasion of his 60th birthday.

Abstract
Influence Analysis is one of the well-known areas of Social Network Analysis. However, discovering influencers from micro-blog networks based on topics has gained recent popularity due to its specificity. Besides, these data networks are massive, continuous and evolving. Therefore, to address the above challenges we propose a dynamic framework for topic modelling and identifying influencers in the same process. It incorporates dynamic sampling, community detection and network statistics over graph data stream from a social media activity management application. Further, we compare the graph measures against each other empirically and observe that there is no evidence of correlation between the sets of users having large number of friends and the users whose posts achieve high acceptance (i.e., highly liked, commented and shared posts). Therefore, we propose a novel approach that incorporates a user's reachability and also acceptability by other users. Consequently, we improve on graph metrics by including a dynamic acceptance score (integrating content quality with network structure) for ranking influencers in micro-blogs. Additionally, we analysed the topic clusters' structure and quality with empirical experiments and visualization.

Abstract
The systematic review reported by this article aimed to analyze and synthesize state-of-the-art studies focused on the cyber resilience of healthcare information systems, namely in terms of (i) their purposes and (ii) methods being used to validate the proposed solutions. An electronic search was conducted, and 14 studies were included in this systematic review after the selection process. The research related to cyber resilience in the context of healthcare information systems is relatively recent and it is increasing, and according to the findings five different purposes were identified: (i) strategies to improve the cyber resilience of healthcare information systems; (ii) methods to design cyber resilient healthcare information systems; (iii) risk assessment; (iv) cyber resilience frameworks; and (v) development of cyber resilient healthcare information systems. Moreover, the solutions reported by the included articles present a low maturity level, which means that further research is required to increase the cyber resilience of healthcare information systems that constitute critical assets of the healthcare provision.

Abstract
Na viragem do milénio, decorrentes sobretudo do Processo de Bolonha e da (r)evolução tecnológica, colocaram-se ao Ensino Superior e aos docentes vários desafios, nomeadamente os relacionados com questões pedagógicas. Tendo essa situação por referência, o artigo apresenta um estudo que analisou a produção académica em Portugal entre 2012-2021, pesquisada com recurso a diversas bases de dados e interpretada por técnicas de análise de frequência e de conteúdo. A análise evidenciou que: o número de artigos publicados em revistas indexadas ou em atas de conferências não foi tão expressivo como a urgência da reflexão que a temática merecia; o número de teses de doutoramento e dissertações de mestrado com foco nas questões pedagógicas no Ensino Superior foi relativamente reduzido; a metodologia desses trabalhos, embora distribuída entre procedimentos de orientação qualitativa, mista e quantitativa, teve menor expressão neste último tipo metodológico; muitos dos autores dos trabalhos académicos são do campo educacional, embora existam também autores de outras áreas científicas; a maior parte dos trabalhos académicos teve como foco a formação pedagógica dos docentes do Ensino Superior, a que se seguiram estudos relativos a práticas pedagógicas e a desafios colocados ao Ensino Superior. A par dessas conclusões, o estudo permitiu identificar limitações que justificam o seu aprofundamento, mas também recomendações para futuros trabalhos de investigação sobre essa temática.

Abstract
Finite-State Automata (FSA) are foundations for modelling, synthesis, verification, and implementation of controllers for manufacturing systems. However, FSA are limited to represent emerging features in manufacturing, such as the ability to recognise and switch contexts. One option is to enrich FSA with parameters that carry details about the manufacturing, which may favour design and control. A parameter can be embedded either on transitions or states of an FSA, and each approach defines its own modelling framework, so that their comparison and integration are not straightforward, and they may lead to different control solutions, modelled, processed and implemented distinctly. In this paper, we show how to combine advantages from parameters in manufacturing the modelling and control. We initially present a background that allows to understand each parameterisation strategy. Then, we introduce a conversion method that translates a design-friendly model into a synthesis-efficient structure. Finally, we use the converted models is synthesis, highlighting their advantages. Examples are used throughout the paper to illustrate and compare our results and tooling support is also provided.

Abstract