Abstract
This article presents a semantics-based program verification framework for critical embedded real-time systems using the worst-case execution time (WCET) as the safety parameter. The verification algorithm is designed to run on devices with limited computational resources where efficient resource usage is a requirement For this purpose, the framework of abstract-carrying code (ACC) is extended with an additional verification mechanism for linear programming (LP) by applying the certifying properties of duality theory to check the optimality of WCET estimates. Further, the WCET verification approach preserves feasibility and scalability when applied to multicore architectural models. The certifying WCET algorithm is targeted to architectural models based on the ARM instruction set and is presented as a particular instantiation of a compositional data-flow framework supported on the theoretic foundations of denotational semantics and abstract interpretation. The data-flow framework has algebraic properties that provide algorithmic transformations to increase verification efficiency, mainly in terms of verification time. The WCET analysis/verification on multicore architectures applies the formalism of latency-rate (LR.) servers, and proves its correctness in the context of abstract interpretation, in order to ease WCET estimation of programs sharing resources.

Abstract
The development and use of computerized decision-support systems in the domain of breast cancer has the potential to facilitate the early detection of disease as well as spare healthy women unnecessary interventions. Despite encouraging trends, there is much room for improvement in the capabilities of such systems to further alleviate the burden of breast cancer. One of the main challenges that current systems face is integrating and translating multi-scale variables like patient risk factors and imaging features into complex management recommendations that would supplement and/or generalize similar activities provided by subspecialty-trained clinicians currently. In this chapter, we discuss the main types of knowledge-objectattribute, spatial, temporal and hierarchical-present in the domain of breast image analysis and their formal representation using two popular techniques from artificial intelligence-Bayesian networks and first-order logic. In particular, we demonstrate (i) the explicit representation of uncertain relationships between low-level image features and high-level image findings (e.g., mass, microcalcifications) by probability distributions in Bayesian networks, and (ii) the expressive power of logic to generally represent the dynamic number of objects in the domain. By concrete examples with patient data we show the practical application of both formalisms and their potential for use in decision-support systems.

Abstract
This work presents a new approach to tune the parameters of the discontinuous component of the Sliding Mode Generalized Predictive Controller (SMGPC) subject to constraints. The strategy employs Particle Swarm Optimization (PSO) to minimize a second aggregated cost function. The continuous component is obtained by the standard procedure, by Sequential Quadratic Programming (SQP), thus yielding a dual optimization scheme. Simulations and performance indexes for a non minimum linear model result in a better performance, improving robustness and tracking accuracy.

Abstract
This paper presents a new approach to efficiently search for suitable compiler pass sequences, a challenge known as phase ordering. Our approach relies on information about the relative positions of compiler passes in compiler pass sequences previously generated for a set of functions when compiling for a specific processor. We enhanced two iterative compiler pass exploration schemes, one relying on simple sequential compiler pass insertion and other implementing an auto-tuned simulated annealing process, with a data structure that holds information about the relative positions of compiler sequences; in order to reduce the set of compiler passes considered for insertion in a given position of a given candidate compiler pass sequence to include only the passes that have a higher probability of performing well on that relative position in the compiler sequence, speeding up the exploration time as a result. We tested our approach with two different compilers and two different targets; the ReflectC and the LLVM compilers, targeting a MicroBlaze processor and a LEON3 processor, respectively. The experimental results show that we can considerably reduce the number of algorithm iterations by a factor of up to more than an order of magnitude when targeting the MicroBlaze or the LEON3, while finding compiler sequences that result in binaries that when executed on the target processor/simulator are able to outperform (i.e. use less CPU cycles) all the standard optimization levels (i.e., we compare against the most performing optimization level flag on each kernel, e.g. -O1, -O2 or -O3 in the case of LLVM) by a geometric mean performance improvement of 1.23x and 1.20x when targeting the MicroBlaze processor, and 1.94x and 2.65x when targetting the LEON3 processor; for each of the two exploration algorithms and two kernel sets considered.

Abstract
In this paper, a mixed-integer linear programing ( MILP) model for the traffic behavior of plug-in electric vehicles ( PEVs) in an urban environment is proposed. It is assumed that any environment can be categorized into different zones based on their urban functions ( e. g. industrial, residential, and commercial). Therefore, the interaction of PEVs that travel between these zones has to be modeled. Besides, it is assumed that in each zone a parking lot ( PL) and individual charging stations exist to provide the required state of charge ( SOC) for PEVs during their daily travel. As a result, the amount of power that these PEVs consume ( rather in PL or charging stations) and the amount of SOC that PEVs carry with them should be precisely computed. The proposed MILP model is applied on two zones urban area with residential and industrial districts and the numerical results prove the proficiency of the model.

Abstract
We study the effects of product differentiation in a Stackelberg model with demand uncertainty for the first mover. We do an ex-ante and ex-post analysis of the profits of the leader and of the follower firms in terms of product differentiation and of the demand uncertainty. We show that even with small uncertainty about the demand, the follower firm can achieve greater profits than the leader, if their products are sufficiently differentiated. We also compute the probability of the second firm having higher profit than the leading firm, subsequently showing the advantages and disadvantages of being either the leader or the follower firm.