Technical reports

Web applications (i.e., applications whose interface is presented to the user via a web browser, whose state is split between a server and a client, and where the only interaction between server and client is through the HTTP protocol) are become more and more widespread, and integrated in most users' everyday work habits. The glue linking the desperate technologies involved, from dynamic HTML to XML RPC, is the Javascript language. Yet, no formal definition of its semantics exists, which in turn makes it impossible to formally prove correctness, liveness and security properties of Web applications. As a first step towards improving this situation, we provide a formal semantics for ECMAScript (standard ECMA-262), by means of an Abstract State Machines (ASMs) specification. We follow the path established by other specification efforts for similar languages (e.g. Java and C#), but in addition we establish a formal trace between parts of our specification and the ECMA standard, thus facilitating the proof of correctness of the specification. More specifically, we define the dynamic semantics of ECMAScript by providing (in terms of ASMs) an interpreter which executes ECMAScript programs. We use an algebra to represent the state of the ECMAScript program, the state of the ECMAScript interpreter, and the state of the host environment (typically, the browser). We assume the necessary syntactic information (namely, the annotated Abstract Syntax Tree (AST) of the given program) to be available. Using ASM we detail a visit of the AST, whose effect is to simulate the execution of the program. In the ECMA standard the behavior of ECMAScript constructs is operationally described using so-called abstract operations (AO), coming as numbered lists of steps. Therefore our interpreter is composed out of two submachines: ECMA-Script and ECMA-AO interpreters. The former invokes the ECMA-AO one to evaluate nodes, simulating AOs used in ECMA standard to describe the production's semantics. We organize the ECMA-AO interpreter rules in such a way that each rule application corresponds to an AO instruction in the ECMA standard. This helps to check the correctness of the ASM model wrt the ECMA standard as well as the correctness of implementations wrt ASM model. Therefore, the state of our interpreter can be mapped via abstraction/refinement functions onto the concrete state of any comformant implementation.

Real-time, indoor user localization, although limited to the current user position, is of great practical importance in many Ambient Assisted Living (AAL) applications. Moreover an accurate prediction of the user next position (even with a short advice) may open a number of new AAL applications that could timely provide the right services in the right place even before the user request them. However, the problem of forecasting the user position is complicated due to the intrinsic difficulty of localization in indoor environments, and to the fact that different paths of the user may intersect at a given point, but they may end in different places. We tackle with this problem by modeling the localization information stream obtained from a Wireless Sensor Network (WSN) using Recurrent Neural Networks implemented as efficient Echo State Networks (ESNs), within the Reservoir Computing paradigm. In particular, we have set up an experimental test-bed in which the WSN produces localization information of a user that moves along a number of different paths, and in which the ESN collects localization information to predict a future position of the user at some given mark points. Our results show that, with an appropriate configuration of the ESN, the system reaches a good accuracy of the prediction also with a small WSN, and that the accuracy scales well with the WSN size. Furthermore, the accuracy is also reasonably robust to variations in the deployment of the sensors. For these reason our solution can be configured to meet the desired trade-off between cost and accuracy.

<p>With the support of the legally-grounded methodology of situation<br />testing, we tackle the problems of discrimination discovery and<br />prevention from a dataset of historical decisions by adopting a<br />variant of k-NN classification. A tuple is labeled as<br />discriminated if we can observe a significant difference of<br />treatment among its neighbors belonging to a protected-by-law<br />group and its neighbors not belonging to it. Discrimination<br />discovery boils down to extracting a classification model from the<br />labeled tuples. Discrimination prevention is tackled by changing<br />the decision value for tuples labeled as discriminated before<br />training a classifier. The approach of this paper overcomes legal<br />weaknesses and technical limitations of existing proposals.</p>

The whole computer hardware industry embraced multicores. For these machines, the extreme optimisation of sequential algorithms is no longer sufficient to squeeze the real machine power, which can be only exploited via thread-level parallelism. Decision tree algorithms exhibit natural concurrency that makes them suitable to be parallelised. This paper presents an approach for easy-yet-efficient porting of an implementation of the C4.5 algorithm on multicores. The approach is based on the FastFlow parallel programming environment. The strength of our porting consists in minimal changes to the original sequential code. In addition to the tree building algorithm, we consider also the so far unaddressed problem of parallelising the error-based pruning with grafting algorithm of C4.5. We devise lower bounds for the forms of parallelisations adopted, and achieve performances close to such bounds.

The paper deals with equilibrium problems (EPs) with nonlinear convex constraints. First, EP is reformulated as a global optimization problem introducing a class of gap functions, in which the feasible set of EP is replaced by a polyhedral approximation. Then, an algorithm is given for solving EP through a descent type procedure related to exact penalties of the gap functions and its global convergence is proved. Finally, the algorithm is tested on a network oligopoly problem with nonlinear congestion constraints<br />

We propose a modification to the (generalized) bundle scheme for minimization of a convex nondifferentiable sum-function in the case where some of the components are ''easy'', that is, they are Lagrangian functions of explicitly known convex programs with ''few'' variables and constraints. This happens in many practical cases, particularly within applications to combinatorial optimization. In this case one can insert in the master problem a suitably modified representation of the original convex subproblem, as an alternative to iteratively inner-approximating it by means of the produced extreme points, thus providing the algorithm with exact information about a part of the objective function, possibly leading to performance improvements. This is shown to happen in at least one relevant application: the computation of tight lower bounds for Fixed-Charge Multicommodity Min-Cost Flow problems.

This paper focuses on client-service interactions distinguishing between three phases: negotiate, commit and execute. The participants negotiate their behaviours, and if an agreement is reached they commit and start an execution which is guaranteed to respect the interaction scheme agreed upon. These ideas are materialised through a calculus of contracts enriched with semiring-based constraints, which allow clients to choose services and to interact with them in a safe way. A concrete representation of these constraints with logic programs and logic program combinations is straightforward, thus reducing constraint solution (and consequently the establishment of a contract) to the execution of a logic program.<br /><br />

We propose a novel generalization of the canonical DC problem (CDC), and we study the convergence of outer approximation algorithms for its solution which use an approximated oracle for checking the global optimality conditions. Although the approximated optimality conditions are similar to those of CDC, this new class of problems is shown to significantly differ from its special case. Indeed, outer approximation approaches for CDC need be substantially modified in order to cope with the more general problem, bringing to new algorithms. We develop a hierarchy of conditions that guarantee global convergence, and we build three different cutting plane algorithms relying on them.<br />

A central issue for parallel applications executed on heterogeneous distributed platforms (e.g. Grids and Clouds) is assuring that performance and cost parameters are optimized throughout the execution. A solution is based on providing application components with adaptation strategies able to select at run-time the best component configuration. In this report we will introduce a preliminary work concerning the exploitation of control-theoretic techniques for controlling the Quality of Service of parallel computations. In particular we will demonstrate how the model-based predictive control strategy can be used based on first-principle performance models of structured parallelism schemes. We will also evaluate the viability of our approach on a first experimental scenario.<br />

\Lname\ is a minimal core calculus that extends Featherweight (generic) Java, \FGJ, with lambda expressions. It has been used to study properties of Simple Closure in Java, including type safety and the abstraction property. Its formalization is based on a reduction semantics and a typing system that extend those of \FGJ. ${\cal F}$ is a source-to-source, translation rule system from Java 1.5 extended with lambda expressions back to ordinary Java 1.5. It has been introduced to study implementation features of closures in Java, including assignment of non local variables and relations with anonymous class objects. In this paper we prove that the two semantics commute. <br /><br />

Most of the decisions in the today's knowledge society are taken<br />on the basis of historical data by extracting models, patterns,<br />profiles, and rules of human behavior in support of (automated)<br />decision making. There is then the need of developing models,<br />methods and technologies for modelling the processes of<br />discrimination analysis in order to discover and prevent<br />discrimination phenomena. In this respect, discrimination analysis<br />from data should build over the large body of existing legal and<br />economic studies. This paper intends to provide a<br />multi-disciplinary survey of the literature on discrimination data<br />analysis, including methods for data collection, empirical<br />studies, controlled experiments, statistical evidence, and their<br />legal requirements and grounds. We cover the following mainstream<br />research lines: labour economic models, (quasi-)experimental<br />approaches such as auditing and controlled experiments,<br />profiling-based approaches such as racial profiling and credit<br />markets, and the recently blooming research on knowledge discovery<br />approaches.

Two classes of nominal automata, namely Usage Automata (UAs) and <br />Variable Finite Automata (VFAs) are considered to express resource con- <br />trol policies over program execution traces expressed by a nominal calcu- <br />lus (Usages). We ?rst analyse closure properties of UAs, and then show <br />UAs less expressive than VFAs. We ?nally carry over VFAs the symbolic <br />technique for model checking Usages against UAs, so making it possi- <br />ble to verify the compliance of a program with a larger class of security <br />properties.

XQuake is a language and system for programming data mining processes over native XML databases in the spirit of inductive databases. It extends XQuery to support KDD tasks. This paper focuses on the features required in the definition of the steps of the mining process. The main objective is to show the expressiveness of the language in handling mining operations as an extension of basic XQuery expressions. To this purpose, the paper offers an extended application in the field of analyzing web logs.<br />

In this report we provide the fundamental results for applying a formal performance modeling of distributed parallel computations described as computation graphs of parallel modules. In our approach parallelism is expressed inside each module (based on structured parallelism schemes) and between different modules that can compose general graph structures. Our methodological approach, based on Queueing Theory and Queueing Network Theory foundations, provides the necessary tools for predicting the steady-state behavior of a parallel computation. <br />

The paper contains the technical complements of the paper, of the same authors, published in the book <span style="font-style: italic;">&quot;Java in Academia and Research&quot;, iConcept Press Ltd, 2011,</span> that describes the extensions of Java 1.5 with Higher Order (H.O. for short) mechanisms. The present complements contain the complete tables of (i) The translation semantics of a form of closure for Java; (ii) The translation semantics of H.O. methods with mc\_parameters as arguments; (iii) The translation semantics of Java extended with the above mechanisms put together; (iv) Theorems, lemmas and proofs of all the properties of the mechanisms and of the semantics discussed in the paper.<br />

Data flow techniques have been around since the early ’70s when they were used in compilers for sequential languages. Shortly after their intro- duction they were also considered as a possible model for parallel comput- ing, although the impact here was limited. Recently, however, data flow has been identified as a candidate for efficient implementation of various programming models on multi-core architectures. In most cases, however, the burden of determining data flow “macro” instructions is left to the programmer, while the compiler/run time system manages only the ef- ficient scheduling of these instructions. We discuss a structured parallel programming approach supporting automatic compilation of programs to macro data flow and we show experimental results demonstrating the fea- sibility of the approach and the efficiency of the resulting “object” code on different classes of state-of-the-art multi-core architectures. The ex- perimental results use different base mechanisms to implement the macro data flow run time support, from plain pthreads with condition variables to more modern and effective lock- and fence-free parallel frameworks. Experimental results comparing efficiency of the proposed approach with those achieved using other, more classical parallel frameworks are also presented.