Abstract
For Anosov flows obtained by suspensions of Anosov diffeomorphisms on surfaces, we show the following type of rigidity result: if a topological conjugacy between them is differentiable at a point, then the conjugacy has a smooth extension to the suspended 3-manifold. This result generalizes the similar ones of Sullivan and Ferreira-Pinto for 1-dimensional expanding dynamics and also a result of Ferreira-Pinto for 2-dimensional hyperbolic dynamics.

Abstract
Modern search engines are evolving beyond ad hoc document retrieval. Nowadays, the information needs of the users can be directly satisfied through entity-oriented search, by ranking the entities or attributes that better relate to the query, as opposed to the documents that contain the best matching terms. One of the challenges in entity-oriented search is efficient query interpretation. In particular, the task of semantic tagging, for the identification of entity types in query parts, is central to understanding user intent. We compare two approaches for semantic tagging, within a single domain, one based on a Sesame triple store and another one based on a Lucene index. This provides a segmentation and annotation of the query based on the most probable entity types, leading to query classification and its subsequent interpretation. We evaluate the run time performance for the two strategies and find that there is a statistically significant speedup, of at least four times, for the index-based strategy over the triple store strategy.

Abstract
This paper presents how the ICT infrastructure developed in the European ENCOURAGE project, centered around a message oriented middleware, enabled energy savings in buildings and households. The components of the middleware, as well as the supervisory control strategy, are overviewed, to support the presentation of the results and how they could be achieved. The main results are presented on three of the pilots of the project, a first one consisting of a single household, a second one of a residential neighborhood, and a third one in a university campus.

Abstract
This paper presents a solar power forecasting scheme, which uses spatial and temporal time series data along with a photovoltaic (PV) power conversion model. The PV conversion model uses the forecast of three different variables, namely, irradiance on the tilted plane, ambient temperature, and wind speed, in order to estimate the power produced by a PV plant at the grid connection terminals. The forecast values are obtained using a spatio-temporal method that uses the data recorded from a target meteorological station as well as data of its surrounding stations. The proposed forecasting method exploits the sparsity of correlations between time series data in a collection of stations. The performance of both the PV conversion model and the spatio-temporal algorithm is evaluated using high-resolution real data recorded in various locations in Italy. Comparison with other benchmark methods illustrates that the proposed method significantly improves the solar power forecasts, particularly over short-term horizons.

Abstract
Port authorities have the need to manage diverse information within the port area under its responsibility regarding their land and sea infrastructures. Through this innovation, which adds value to the port and its activity, it is made an interconnection of strategic areas, with the provision and sharing of structured data in a georeferenced environment. This work presents an innovative platform, based on various modules and allows effective control and efficient management of operations, processes and requirements associated with any sea port. The developed modules are designed to support the activities of business processes in the following areas of the port administration: Heritage, Hydrography, Port Traffic, Dominial, Studies and Works, Safety and Environment. Most of these modules were pioneers in the integration with business process management of portuguese ports of Leixoes and Viana do Castelo.

Abstract
Concurrent programming is dominated by thread based solutions with lock based critical sections. Careful attention has to be paid to avoid race and deadlock conditions. Real-Time for The Masses (RTFM) takes an alternative language approach, introducing tasks and named critical sections (via resources) natively in the RTFM-core language. RTFM-core programs can be compiled to native C-code, and efficiently executed onto single-core platforms under the Stack Resource Policy (SRP) by the RTFM-kernel. In this paper we formally define the well-formedness criteria for SRP based resource management, and develop a certified (formally proven) implementation of the corresponding compilation from nested critical sections of the input RTFM-core program to a resulting flat sequence of primitive operations and scheduling primitives. Moreover we formalise the properties for resource ceilings under SRP and develop a certified algorithm for their computation. The feasibility of the described approach is shown through the adoption of the Why3 platform, which allows the necessary verification conditions to be automatically generated and discharged through a variety of automatic external SMT-solvers and interactive theorem provers. Moreover, Why3 supports the extraction of certified Ocaml code for proven implementations in WhyML. As a proof of concept the certified extracted development is demonstrated on an example system. © 2016 IEEE.