Search

After a short review of the MiFID regulations and the RAF, the paper identifies the link between them which allows to mitigate a balance sheet risk sustained by the financial intermediary and, at the same time, to improve its stability and value creation, through a maximization of customer loyalty. The client’s attitude towards risk can be summarized in these terms: "I don't like risk, but I like to win". Thus, a three-dimensional approach towards expected utility is suggested for estimating risk tolerance: risk aversion, loss aversion and reflection. In addition, a definition of the client's financial objectives is required, combined with greater disclosure - which allows the construction of a financial statement – to attest that risk-taking is indeed a luxury, as indicated by the metrics of the discretionary wealth ratio, and therefore, of the Standard of Living Risk (SLR). The next step consists in the determination of a set of portfolios along the efficient frontier where risk is represented by the expected shortfall, the determination of which belongs to a Generalized Extreme Value Theory logic. The client's objectives are described in terms of probability of success, where the latter is a function of an initial endowment, a potential positive contribution of financial resources over time as well as an expected return level. The above is expressed through a practical case that envisages the determination of a set of EGPF portfolios and the identification of the specific portfolio, obtained as a solution to a static and dynamic optimization problem, where the objectives have been formalized through the calculation of the associated utility.

Objectives: Until 2018, cervical cancer (CC) was clinically staged; however, it was frequently under-staged. For this reason, in 2018, the International Federation of Gynecology and Obstetrics (FIGO) incorporated the imaging assessment into the staging of this malignancy. The aim of this review is to discuss available data regarding the role of imaging in the diagnosis, pretreatment staging, and how an adequate radiological evaluation could assist in the treatment planning for CC. Mechanism: An extensive literature search was conducted to identify relevant studies across various databases, including articles addressing topics related to imaging used in CC. The selected articles underwent thorough examination and evaluation to identify studies that met the objectives of this review, taking into account the specified inclusion and exclusion criteria. Subsequently, relevant data were extracted and analyzed for each article. Findings in Brief: Transvaginal ultrasound (TVS) and transrectal ultrasound (TRUS) have been shown to be accurate diagnostic tools to assessing the local spread of CC disease. Currently, magnetic resonance imaging (MRI) appears to offer the highest sensitivity, specificity, and accuracy in detecting parametrial and stromal invasion, as well as tumor size. Computed tomography (CT) and contrast-enhanced (CE)-CT are considered the best imaging modalities for the detection of lymph node metastases. However, positron emission tomography (PET) has demonstrated notable precision and exhibited high negative predictive value in predicting the pelvic nodal status during the early-stage diagnosis of CC diagnosis. Radiomics represents a newly introduced field of translational research with the potential to predict several clinically and pathological relevant variables in cervical carcinoma patients. These variables include disease staging, histological type, lymph node status, probability of recurrence, and estimated survival. Conclusions: Imaging plays an indispensable role in diagnosis, tumor staging, and monitoring the evolution of pathology in response to therapies over time. It provides physicians with the indispensable tool for optimal regulation of therapeutic strategy.

Endometrial cancer (EC) is one of the most common gynecological malignancies in Western countries. Traditionally, loco-reginal dissemination and histological characteristics are the main prognostic factors. Nowadays, molecular and genomic profiling showed exciting results in terms of prognostication. According to the data provided by The Cancer Genome Atlas and other studies, molecular and genomic profiling might be useful in identifying patients al low, intermediate, and high risk of recurrence. However, data regarding the therapeutic value are scant. Several prospective studies are ongoing to identify the most appropriate adjuvant strategy in EC patients, especially for those with positive nodes and low volume disease. The molecular classification has offered the possibility to improve the risk stratification and management of EC. The aim of this review is to focus on the evolution of molecular classification in EC and its impact on the research approach and on clinical management. Molecular and genomic profiling might be useful to tailor the most appropriate adjuvant strategies in apparent early-stage EC.

It is known that the verification of imperative, functional, and logic programs can be reduced to the satisfiability of constrained Horn clauses (CHCs), and this satisfiability check can be performed by using CHC solvers, such as Eldarica and Z3. These solvers perform well when they act on simple constraint theories, such as Linear Integer Arithmetic and the theory of Booleans, but their efficacy is very much reduced when the clauses refer to constraints on inductively defined structures, such as lists or trees. Recently, we have presented a transformation technique for eliminating those inductively defined data structures, and hence avoiding the need for incorporating induction principles into CHC solvers. However, this technique may fail when the transformation requires the use of lemmata whose generation needs ingenuity. In this paper we show, through an example, how during the process of transforming CHCs for eliminating inductively defined structures one can introduce suitable predicates, called difference predicates, whose definitions correspond to the lemmata to be introduced. Through a second example, we show that, whenever difference predicates cannot be introduced, we can introduce, instead, auxiliary queries which also correspond to lemmata, and the proof of these lemmata can be done by showing the satisfiability of those queries.

The proof of a program property can be reduced to the proof of satisfiability of a set of constrained Horn clauses (CHCs) which can be automatically generated from the program and the property. In this paper we have conducted a case study in Horn clause verification by considering several sorting programs with the aim of exploring the effectiveness of a transformation technique which allows us to eliminate inductive data structures such as lists or trees. If this technique is successful, we derive a set of CHCs with constraints over the integers and booleans only, and the satisfiability check can often be performed in an effective way by using state-of-the-art CHC solvers, such as Eldarica or Z3. In this case study we have also illustrated the usefulness of a companion technique based on the introduction of the so-called difference predicates, whose definitions correspond to lemmata required during the verification. We have considered functional programs which implement the following kinds of sorting algorithms acting on lists of integers: (i) linearly recursive sorting algorithms, such as insertion sort and selection sort, and (ii) non-linearly recursive sorting algorithms, such as quicksort and mergesort, and we have considered the following properties: (i) the partial correctness properties, that is, the orderedness of the output lists, and the equality of the input and output lists when viewed as multisets, and (ii) some arithmetic properties, such as the equality of the sum of the elements before and after sorting.

Dynamically typed languages, like Erlang, allow developers to quickly write programs without explicitly providing any type information on expressions or function definitions. However, this feature makes those languages less reliable than statically typed languages, where many runtime errors can be detected at compile time. In this paper, we present a preliminary work on a tool that, by using the well-known techniques of metaprogramming and symbolic execution, can be used to perform bounded verification of Erlang programs. In particular, by using Constraint Logic Programming, we develop an interpreter that, given an Erlang program and a symbolic input for that program, returns answer constraints that represent sets of concrete data for which the Erlang program generates a runtime error.

Verification conditions (VCs) are logical formulas whose satisfiability guarantees program correctness. We consider VCs in the form of constrained Horn clauses (CHC) which are automatically generated from the encoding of (an interpreter of) the operational semantics of the programming language. VCs are derived through program specialization based on the unfold/fold transformation rules and, as it often happens when specializing interpreters, they contain unnecessary variables, that is, variables which are not required for the correctness proofs of the programs under verification. In this paper we adapt to the CHC setting some of the techniques that were developed for removing unnecessary variables from logic programs, and we show that, in some cases, the application of these techniques increases the effectiveness of Horn clause solvers when proving program correctness.

We present a verification technique for program safety that combines Iterated Specialization and Interpolating Horn Clause Solving. Our new method composes together these two techniques in a modular way by exploiting the common Horn Clause representation of the verification problem. The Iterated Specialization verifier transforms an initial set of verification conditions by using unfold/fold equivalence preserving transformation rules. During transformation, program invariants are discovered by applying widening operators. Then the output set of specialized verification conditions is analyzed by an Interpolating Horn Clause solver, hence adding the effect of interpolation to the effect of widening. The specialization and interpolation phases can be iterated, and also combined with other transformations that change the direction of propagation of the constraints (forward from the program preconditions or backward from the error conditions). We have implemented our verification technique by integrating the VeriMAP verifier with the FTCLP Horn Clause solver, based on Iterated Specialization and Interpolation, respectively. Our experimental results show that the integrated verifier improves the precision of each of the individual components run separately.

We present a method for verifying partial correctness properties of imperative programs that manipulate integers and arrays by using techniques based on the transformation of constraint logic programs (CLP). We use CLP as a metalanguage for representing imperative programs, their executions, and their properties. First, we encode the correctness of an imperative program, say prog, as the negation of a predicate 'incorrect' defined by a CLP program T. By construction, 'incorrect' holds in the least model of T if and only if the execution of prog from an initial configuration eventually halts in an error configuration. Then, we apply to program T a sequence of transformations that preserve its least model semantics. These transformations are based on well-known transformation rules, such as unfolding and folding, guided by suitable transformation strategies, such as specialization and generalization. The objective of the transformations is to derive a new CLP program TransfT where the predicate 'incorrect' is defined either by (i) the fact 'incorrect.' (and in this case prog is not correct), or by (ii) the empty set of clauses (and in this case prog is correct). In the case where we derive a CLP program such that neither (i) nor (ii) holds, we iterate the transformation. Since the problem is undecidable, this process may not terminate. We show through examples that our method can be applied in a rather systematic way, and is amenable to automation by transferring to the field of program verification many techniques developed in the field of program transformation.

Il Laboratorio di Meccanica del Volo (MDVLab) dell’Università di Bologna nasce nel 2006 presso la Seconda Facoltà di Ingegneria e la sua attività di ricerca riguarda principalmente problematiche di modellazione, simulazione e controllo del volo atmosferico e spaziale. Un'intensa collaborazione con l’Istituto Nazionale di Geofisica e Vulcanologia (INGV) ha consentito di estendere le proprie conoscenze al di fuori del settore aerospaziale, presentando oggi un’ampia offerta di tecnologie per l’Osservazione della Terra nell'ambito di progetti in cui MDVLab è coinvolto insieme ad INGV per l’impiego di velivoli non abilitati per applicazioni di gestione del rischio sismico, vulcanico ed ambientale. Flight testing with thermal camera Remote sensing from satellites or aircraft represents an impor-tant tool for the monitoring and management of catastrophic events. For some rapidly evolving phenomena (e.g. volcanic events, wildfires) they both show two relevant limits: long revisiting time (satellites) and the high cost and high human risk for monitoring. Unmanned Aircraft Veicle (UAV) because of their autonomous flight and real time telemetry transmis-sion offer a good solution to these limitations.To explore the operational aspects of such UAV deployments for example in volcanology, INGV in partnership with MavLab department of University of Bologna (Unibo) developed a UAV system and actually are carrying on integration studies and testing of sci-entific payloads. The payload is thermal camera. it has a light weight of 67.5g while the spectral response is in the 7-14mi-cron spectral range. The integration activities, the on board installation and results of the first in flight thermal acquisition experiment realized on July 30 2011, in Italy, are presented.

MDVLab: a flight over Antarctica The Flight Mechanics Laboratory (MDVLab) of the University of Bologna was born in 2006 at the Second Faculty of Engineering. The research activity mainly covers problems of modeling, simulation and control of atmospheric and spatial flight. Thanks to the intense collaboration with the National Institute of Geophysics and Volcanology (INGV), the workgroup has extended its knowledge beyond the aerospatial field, showing a wide offer of technologies for the Observation of the Earth. An important project in wich MDVLab is involved with INGV regards the use of unmanned aircrafts for magnetic field measurements in Antarctica; in this paper the acquisition system is described and the first experimental results are shown.