Abstract
The use of model checking tools allows for the formal verification of properties over models of systems, improving their robustness. However, these tools are challenging to use, and their results require much work of interpretation to communicate to stakeholders. To address this issue, the IVY Workbench offers a plethora of options to make the process of creating and understanding the models, properties and results of the verification process more accessible, with a particular focus on interactive computing systems. Despite this, there is still a significant requirement of expertise to use the tool. To solve this, an approach to provide structured natural language explanations for the results of model checking-based tools is being developed, to be later incorporated into the IVY Workbench. This paper presents the current state of the approach's development, stating its objective and what results can already be achieved.

Abstract

Abstract
Model checkers can automatically verify a system’s behavior against temporal logic properties. However, analyzing the counterexamples produced in case of failure is still a manual process that requires both technical and domain knowledge. However, this step is crucial to understand the flaws of the system being verified. This paper presents a language created to support the generation of natural language explanations of counterexamples produced by a model checker. The language supports querying the properties and counterexamples to generate the explanations. The paper explains the language components and how they can be used to produce explanations. © Ezequiel José Veloso Ferreira Moreira and José Creissac Campos.

Abstract
The second workshop on HCI Engineering Education continued the effort of the IFIP Working Group 2.7/13.4 on User Interface Engineering by discussing the issues and identifying the opportunities in teaching and learning Human-Computer Interaction (HCI) Engineering. The workshop attracted eight papers covering different teaching contexts, ranging from massive university courses, passing through different teaching experiences in specific academic curricula, and even teaching engineering concepts to children. In addition, the workshop received input for improving and adapting the repository material to the dynamic nature of this field. The discussion after the presentation of the contributions focused on how to model competencies, the support to interdisciplinary work, the overall course design, the recruitment of the students and the provision of educational resources, paving the way for further editions of the workshop.

Abstract
This paper leverages the outcomes of the first workshop on HCI Engineering Education [4] to create an online repository where the community can share content relevant to HCI. The repository takes advantage of the functionalities of the Git file versioning system to support presenting and adding content. The paper describes the structure of the repository and the process for adding new content. In addition, we propose an adaptation of the framework for presenting teaching samples, supporting more flexibility in the application of educational material for different teaching objectives. The new presentation format starts with describing a design problem and emphasises the students' applied understanding of conceptual and theoretical knowledge. The presentation format is demonstrated and discussed by the example of an end-user design tool for mobile data collection.

Abstract
Humans are good at understanding subjective or vague statements which, however, are hard to express in classical logic. Fuzzy logic is an evolution of classical logic that can cope with vague terms by handling degrees of truth and not just the crisp values true and false. Logic is the formal basis of computing, enabling the formal design of systems supported by tools such as model checkers and theorem provers.This paper shows how a model checker such as Alloy can evolve to handle both classical and fuzzy logic, enabling the specification of high-level quantitative relational models in the fuzzy domain. In particular, the paper showcases how QAlloy-F (a conservative, general-purpose quantitative extension to standard Alloy) can be used to tackle fuzzy problems, namely in the context of validating the design of fuzzy controllers. The evaluation of QAlloy-F against examples taken from various classes of fuzzy case studies shows the approach to be feasible.