In the brain, neuronal cells located in different functional regions communicate through a dense structural network of axons known as the white matter (WM) tissue. Bundles of axons that share similar pathways characterize the WM anatomy, which can be investigated in-vivo thanks to the recent advances of magnetic resonance (MR) techniques. Diffusion MR imaging combined with tractography pipelines allows for a virtual reconstruction of the whole WM anatomy of in-vivo brains, namely the tractogram. It consists of millions of WM fibers as 3D polylines, each approximating thousands of axons. From the analysis of a tractogram, neuroanatomists can characterize well-known white matter structures and detect anatomically non-plausible fibers, which are artifacts of the tractography and often constitute a large portion of it. The accurate characterization of tractograms is pivotal for several clinical and neuroscientific applications. However, such characterization is a complex and time-consuming process that is difficult to be automatized as it requires properly encoding well-known anatomical priors. In this thesis, we propose to investigate the encoding of anatomical priors with a supervised deep learning framework. The ultimate goal is to reduce the presence of artifactual fibers to enable a more accurate automatic process of WM characterization. We devise the problem by distinguishing between volumetric and non-volumetric representations of white matter structures. In the first case, we learn the segmentation of the WM regions that represent relevant anatomical waypoints not yet classified by WM atlases. We investigate using Convolutional Neural Networks (CNNs) to exploit the volumetric representation of such priors. In the second case, the goal is to learn from the 3D polyline representation of fibers where the typical CNN models are not suitable. We introduce the novelty of using Geometric Deep Learning (GDL) models designed to process data having an irregular representation. The working assumption is that the geometrical properties of fibers are informative for the detection of tractogram artifacts. As a first contribution, we present StemSeg that extends the use of CNNs to detect the WM portion representing the waypoints of all the fibers for a specific bundle. This anatomical landmark, called stem, can be critical for extracting that bundle. We provide the results of an empirical analysis focused on the Inferior Fronto-Occipital Fasciculus (IFOF). The effective segmentation of the stem improves the final segmentation of the IFOF, outperforming with a significant gap the reference state of the art. As a second and major contribution, we present Verifyber, a supervised tractogram filtering approach based on GDL, distinguishing between anatomically plausible and non-plausible fibers. The proposed model is designed to learn anatomical features directly from the fiber represented as a 3D points sequence. The extended empirical analysis on healthy and clinical subjects reveals multiple benefits of Verifyber: high filtering accuracy, low inference time, flexibility to different plausibility definitions, and good generalization. Overall, this thesis constitutes a step toward characterizing white matter using deep learning. It provides effective ways of encoding anatomical priors and an original deep learning model designed for fiber.

Autonomous systems must be able to detect and promptly react to faults. Fault Detection and Identification components (FDI) are in charge of detecting the occurrence of faults. The FDI depends on the concrete design of the system, needs to take into account how faults might interact, and can only have a partial view of the run-time state through sensors. For these reasons, the development of the FDI and certification of its correctness and quality are difficult tasks. This difficulty is compounded by the fact that current approaches for verification of the FDI rely on manual inspection and testing. Motivated by industrial case-studies from the European Space Agency, this thesis proposes a formal foundation for FDI design that covers specification, validation, verification, and synthesis. The Alarm Specification Language (ASLk) is introduced in order to formally capture a set of interesting and desirable properties of the FDI components. ASLk is equipped with a semantics based on Temporal Epistemic Logic, thus enabling reasoning about partially observable systems. Automated reasoning techniques can then be applied to perform validation, verification, and synthesis of the FDI. This formal process guarantees that the generated FDI satisfies the designer expectations. The problems deriving from this process were out of reach for existing model-checking techniques. Therefore, we develop novel and efficient techniques for model-checking temporal epistemic logic over infinite state systems.

Any form of model-based reasoning is limited by the adherence of the model to the actual reality. Scheduling is the problem of finding a suitable timing to execute a given set of activities accommodating complex temporal constraints. Planning is the problem of finding a strategy for an agent to achieve a desired goal given a formal model of the system and the environment it is immersed in. When time and temporal constraints are considered, the problem takes the name of temporal planning. A common assumption in existing techniques for planning and scheduling is controllability of activities: the agent is assumed to be able to control the timing of starting and ending of each activity. In several practical applications, however, the actual timing of actions is not under direct control of the plan executor. In this thesis, we focus on this temporal uncertainty issue in scheduling and in temporal planning: we propose to natively express temporal uncertainty in the model used for reasoning. We first analyze the state-of-the-art on the subject, presenting a rationalization of existing works. Second, we show how Satisfiability Modulo Theory (SMT) solvers can be exploited to quickly solve different kinds of query in the realm of scheduling under uncertainty. Finally, we address the problem of temporal planning in domains featuring real-time constraints and actions having duration that is not under the control of the planning agent.

In this work we provided a contribution in the specific context of verbal humor generation, focused on computational creation of humorous texts. The goal consisted of the design and implementation of a tool for the automatic generation of short humorous expressions. We focused on humorous puns generated through the variation of familiar expressions, performed via lexical substitution. Phonetic and semantic features are employed to select the appropriate substitution. We have chosen a corpus-based approach, in line with a tendency prevailing in the computational linguistics field. A number of textual corpora and dictionaries were employed. We have developed some of these resources (WordNet-Affect and Affective-Weight) in an early stage of the research. The system can be used as a testbed for the empirical investigation of various aspects of verbal humor. More specifically, it can be used to study the correlation between linguistic parameters of humorous expressions and appraisal dimensions that are part of the cognitive process of humor understanding. In the last phase of the work, we developed two exploratory applications: a prototype was developed as a first component of a system in which task-oriented assistance and humorous feedback can be integrated to achieve frustration reduction. The other application developed is a tool for the collaborative creation of puns. In this system, the pun generator is integrated with a graphical user interface based on a dynamic graph, helping the exploration of different creative solutions.

Formal methods are becoming increasingly important for debugging and verifying hardware and software systems, whose current complexity makes the traditional approaches based on testing increasingly-less adequate. One of the most promising research directions in formal verification is based on the exploitation of Satisfiability Modulo Theories (SMT) solvers. In this thesis, we present MathSAT, a modern, efficient SMT solver that provides several important functionalities, and can be used as a workhorse engine in formal verification. We develop novel algorithms for two functionalities which are very important in verification -- the extraction of unsatisfiable cores and the generation of Craig interpolants in SMT -- that significantly advance the state of the art, taking full advantage of modern SMT techniques. Moreover, in order to demonstrate the usefulness and potential of SMT in verification, we develop a novel technique for software model checking, that fully exploits the power and functionalities of the SMT engine, showing that this leads to significant improvements in performance.

Every human being is familiar to the experience of reminiscence: recalling and revisiting our past memories. We reminisce to create our identities. We reminisce to maintain our relationships. We reminisce to review our lives. And we also reminisce together. This dissertation develops around the topic of how IT stimulates reminiscence, motivated by its proven benefits in peopleâ s well-being and its prevalence across all stages of life. The focus is set on older adults, with the overall goal of fostering intergenerational social interactions (that is, interactions between older adults and younger generations). This thesis is motivated by the current interest on active ageing as an emergent way of life, with better and more opportunities for health, participation and security. As the world ageing population continues to increase and the average life expectancy of people increasing every year, there is a growing need for understanding the ageing phenomena, and particularly, for designing human centered information technologies (IT) that enhance opportunities of social participation as people age. Within this scenario, this dissertation addresses the following research questions using a participatory approach to research and design: (i) what is the role of IT in enabling a more happy and active ageing?; (ii) in doing so, how can IT stimulate intergenerational social interactions?, and (iii) can IT-supported social reminiscence facilitate these interactions and make of them an enjoyable experience?. To answer these questions, we leverage upon a participatory action research approach to gain an understanding of the topic, moving later to the participatory design of IT for social reminiscence and finally, evaluating how IT supports the practice of social reminiscence in a face-to-face intergenerational context. The contributions of this dissertation can be summarized as follows: - Knowledge: an understanding of what role IT can play in supporting, stimulating and accompanying active ageing and social interactions through the practice of reminiscence. - Model: a conceptual model of the different stages of IT-supported social reminiscence sessions, and an extended model of the design spaces for intergenerational engagement. - System: an exemplary socio-technical system that fits the aforementioned roles, including a knowledge base and algorithms to support contextual stimulation of reminiscence, using multimedia resources that are publicly available on the web. - Evaluation: quantitative and qualitative results obtained from observing the use of our system in a real intergenerational context.

Formal methods are becoming increasingly important for debugging and verifying hardware and software systems, whose current complexity makes the traditional approaches based on testing increasingly-less adequate. One of the most promising research directions in formal verification is based on the exploitation of Satisfiability Modulo Theories (SMT) solvers. In this thesis, we present MathSAT, a modern, efficient SMT solver that provides several important functionalities, and can be used as a workhorse engine in formal verification. We develop novel algorithms for two functionalities which are very important in verification -- the extraction of unsatisfiable cores and the generation of Craig interpolants in SMT -- that significantly advance the state of the art, taking full advantage of modern SMT techniques. Moreover, in order to demonstrate the usefulness and potential of SMT in verification, we develop a novel technique for software model checking, that fully exploits the power and functionalities of the SMT engine, showing that this leads to significant improvements in performance.

This thesis introduces SKOs (Scientific Knowledge Object) a specification for capturing the knowledge and artifacts that are produced by the scientific research processes. Aiming to address the current existing limitations of scientific production this specification is focused on reducing the work overhead of scientific creation, being composable and reusable, allow continuous evolution and facilitate collaboration and discovery among researchers. To do so it introduces four layers that capture different aspects of the scientific knowledge: content, meaning, ordering and visualization.

Access to geographic information has radically changed in the past decade. Previously, it was a specific task, for which complex desktop Geographic Information Systems (GISs) were built, and geographic data was maintained locally, managed by a restricted number of technicians. With the significant impact of the world-wide-web, an increasing number of different geographic services became available from heterogeneous sources. To support interoperability among different providers and users, GIS agencies have started to adopt Spatial Data Infrastructure (SDI) models. Usually, each SDI service provider publishes and gathers geographic information based on its background knowledge. Hence, discovering, chaining, and using services require a semantic interoperability level between different providers. This problem is typically referred as the need for 'semantic interoperability among autonomous and heterogeneous systems' and it is a challenge for current SDIs, due to their distributed architecture. This thesis provides a framework to approach the semantic heterogeneity problem in the field of geo-services - services that deal with the generation and management of geographical information - among distributed SDIs. The framework is based on: (i) a peer-to-peer (P2P) view of the semantics of web service coordination, implemented by using the OpenKnowledge system and (ii) the use of a specific semantic matching solution called Structure Preserving Semantic Matching (SPSM). SPSM is a basic module of OpenKnowledge as it enables web service discovery and integration by using semantic matching between invocations of web services and web service descriptions. We applied the OpenKnowledge system on a realistic emergency response scenario and selected SDI services. We modeled an emergency response scenario, i.e., a potential flooding event in the area of Trento. The scenario is based on the past experience and actual emergency plans as collected from interviews with personnel of the involved institutions and from related documents. Within this emergency response scenario a detailed implementation of selected SDI services is presented, namely the gazetteer, map and download services. The SPSM solution has been assessed on a set of GIS ESRI ArcWeb services. Two kinds of experiments have been conducted: the first experiment includes matching of original web service signatures with synthetically altered ones. In the second experiment a manual classification of the GIS dataset has been compared to the unsupervised one produced by SPSM. The evaluation results demonstrate robustness and good performance of the SPSM approach on a large (ca. 700.000) number of matching tasks. In the first experiment a high overall matching relevance quality (F-measure) was obtained (over 55%). In the second experiment the best F-measure value exceeded 50% for the given GIS operations set. SPSM performance is good, since the average execution time per matching task was 43 ms. This suggests that SPSM could be employed to find similar web service implementations at runtime. The aforementioned results suggest the practical real time application of the SPSM approach to: (i) discovering geo-services from specific geographic information catalogs, (ii) composing specific geo-processing services, (iii) supporting coordination of geo-sensor networks, and (iv) supporting geo-data discovering and integration.

The use of intelligent presentation systems within a museum is a well-established practice. This thesis deals with connecting the museum experience with novel cultural experiences in the outside world, with attention to the individual in recognizing opportunities and delivering tailored presentations. Our goal is to help keep the user connected to the cultural experience and to help develop further knowledge and intellectual pleasure after the museum visit. The specific goal of this research is to explore the potential of technology 1) to define contextual opportunities†, 2) to identify these contextual opportunities, 3) to select relevant material, and 4) to deliver it, given the right context, in the most appropriate way for the specific user. We review the field of personalized cultural heritage experience and technology, and related research areas, needed to serve as a grounded basis for ideas developed in the framework. We examine user preferences by reviewing data from two surveys, we conducted, in order to develop additional (from those in the background) inputs (points) for the theoretical framework model. We then describe our theoretical frameworks, both finding the next place to go, and connecting back to previous experiences. We describe the System Architecture and give three concrete examples of use cases. We report on an initial evaluation of the system (and the underlying theoretical framework) by a visitor study, followed by a discussion of possible implications.