Abstract
Program verification tools use verification condition generators to produce logical formulas whose validity implies that the program is correct with respect to its specification. Different tools produce different conditions, and the underlying algorithms have not been properly exposed or explored so far. In this paper we consider a simple imperative programming language, extended with assume and assert statements, to present different ways of generating verification conditions. We study the approaches with experimental results originated by verification conditions generated from the intermediate representation of LLVM.

Abstract
Humanoid soccer robots must be able to carry out their tasks in a highly dynamic environment which requires responsive omnidirectional walking. This paper explains a new omnidirectional walking engine for a humanoid soccer robot that mainly consists of a foot planner, a zero moment point (ZMP) trajectory generator, a centre of mass (CoM) calculator and an active balance feedback loop. An analytical approach is presented for generating the CoM trajectory, in which the cart-table motion of the equations is solved using the Fourier approximation of the ZMP. With this approach, we propose using a new time segmentation approach in order to parametrize the double-support phase. An active balance method is also proposed which keeps the robot's trunk upright when faced with environmental disturbances. The walking engine is tested on both simulated and real NAO robots. Our results are encouraging given the fact that the robot performs favourably, walking quickly and in a stable manner in any direction in comparison with the best RoboCup 3D soccer simulation teams for which the same simulator is used. In addition, the proposed analytical Fourier-based approach is compared with the well-established numerical ZMP dynamics control method. Our results show that the presented analytical approach involves less time and complexity and better accuracy compared with the ZMP preview control method.

Abstract
In this study the case of the energy consumption profile of the Aristotle University of Thessaloniki, in Greece, is presented and statistically analyzed by clustering methods on the basis of seasonal daily load curves and load shape factors, using data from real-time measurements. The results indicate that the categorization of active power demand in university buildings is an extremely useful tool for understanding and predicting the seasonal, hourly and daily energy consumption changes, which is the first step towards adopting energy efficiency policies in such scale premises as well as performing demand-side actions aiming to achieve a more economical and environmentally sustainable energy usage.

Abstract
The main goal of recommender systems is to assist users in finding items of their interest in very large collections. The use of good automatic recommendation promotes customer loyalty and user satisfaction because it helps users to attain their goals. Current methods focus on the immediate value of recommendations and are evaluated as such. This is insufficient for long term goals, either defined by users or by platform managers. This is of interest in recommending learning resources to learn a target concept, and also when a company is organizing a campaign to lead users to buy certain products or moving to a different customer segment. Therefore, we believe that it would be useful to develop recommendation algorithms that promote the goals of users and platform managers (e.g. e-shop manager, e-learning tutor, ministry of culture promotor). Accordingly, we must define appropriate evaluation methodologies and demonstrate the concept on practical cases.

Abstract
Application frameworks are a powerful technique for large-scale reuse but often very hard to learn from scratch. Although good documentation helps on reducing the learning curve, it is often found lacking, and costly, as it needs to attend different audiences with disparate learning needs. When code and documentation prove insufficient, developers turn to their network of experts. The lack of awareness about the experts, interrupting the wrong people, and experts unavailability are well known hindrances to effective collaboration. This paper presents the DRIVER platform, a collaborative learning environment for framework users to share their knowledge. It provides the documentation on a wiki, where the learning paths of the community of learners can be captured, shared, rated, and recommended, thus tapping into the collective knowledge of the community of framework users. The tool can be obtained at http://bit.ly/driverTool.

Abstract
Reject option is a technique used to improve classifier’s reliability in decision support systems. It consists in withholding the automatic classification of an item, if the decision is considered not sufficiently reliable. The rejected item is then handled by a different classifier or by a human expert. The vast majority of the works on this issue has been concerned with the development of reject option mechanisms to be used by supervised learning architectures (e.g., MLP, LVQ or SVM). In this paper, however, we aim at proposing alternatives to this view, which are based on the self-organizing map (SOM), originally an unsupervised learning scheme, but that has also been successfully used in the design of prototype-based classifiers. The basic hypothesis we defend is that it is possible to design SOM-based classifiers endowed with reject option mechanisms whose performances are comparable to or better than those achieved by standard supervised classifiers. For this purpose, we carried out a comprehensively evaluation of the proposed SOM-based classifiers on two synthetic and three real-world datasets. The obtained results suggest that the proposed SOM-based classifiers consistently outperform standard supervised classifiers. © 2015 The Natural Computing Applications Forum