Abstract
Cryptographic software development is a challenging field: high performance must be achieved, while ensuring correctness and compliance with low-level security policies. CAO is a domain specific language designed to assist development of cryptographic software. An important feature of this language is the design of a novel type system introducing native types such as predefined sized vectors, matrices and bit strings, residue classes modulo an integer, finite fields and finite field extensions, allowing for extensive static validation of source code. We present the formalisation, validation and implementation of this type system. © 2012 Springer-Verlag.

Abstract
In this paper, an approach is presented that identifies music samples which are difficult for current state-of-the-art beat trackers. In order to estimate this difficulty even for examples without ground truth, a method motivated by selective sampling is applied. This method assigns a degree of difficulty to a sample based on the mutual disagreement between the output of various beat tracking systems. On a large beat annotated dataset we show that this mutual agreement is correlated with the mean performance of the beat trackers evaluated against the ground truth, and hence can be used to identify difficult examples by predicting poor beat tracking performance. Towards the aim of advancing future beat tracking systems, we demonstrate how our method can be used to form new datasets containing a high proportion of challenging music examples.

Abstract
Logic programming is well suited for declaratively solving computational problems that require knowledge representation and reasoning. Object-oriented languages, on the other hand, are well suited for modeling real-world concepts and profit from rich ecosystems developed around them, which are often missing from logic languages. For applications that require both the declarative power of logic programming and the rich modeling expressiveness and development environments offered by object-oriented languages, there is a need for reconciling both worlds. LogicObjects is our linguistic symbiosis framework for integrating Prolog within the Java language. It extends Java with annotations that allow Java programs to interact transparently and automatically with Prolog programs. Copyright 2012 ACM.

Abstract
The Mike Basin - Water Quality modelling system was applied to the hydrographical basin of Sordo river located in the northeast of Portugal, in the region of Trasos-Montes and Alto Douro. This model allows the simulation of diffuse pollution caused by nitrate concentration in a small hydrographical basin (located in the demarcated region of the Port wine). The model allows the creation of a set of scenarios aiming at an effective planning of the basin under study. The available data for the drainages calculation were the monthly average effective rainfall between the years of 1960 and 2008. The Climate-change was predicted by the scenarios created in SIAM II and were simulated with the HadRM3 model. The limit quantities of nitrate present in the water should not contain over 25 mg/l; this is the maximum recommended value, and should not exceed 50 mg/l, this is the maximum allowable value by Portuguese law. We created simulation scenarios using the fertilizers produced by the bovine cattle and change of the agricultural uses or crops in this basin. For 2010 the fertilizers used were comprised between the recommended and the allowable maximum values. For 2071 the fertilizers were above the maximum allowable value. With these scenarios we found a 40% increase in nitrate levels due to climate change between the years 2010 and 2071.

Abstract
The IEC 61508 standard recognizes the programming languages defined in IEC 61131-3 as being appropriate for safety-related applications, and suggests the use of static data type analysis of the source code. In this context, we have added a data type semantic verifier to the MatlEC compiler - an open source ST, IL and SFC code translator to ANSI C. In so doing, we have identified several issues related to the definition of the semantics of the IL and ST programming languages, as well as with the data type model defined in IEC 61131-3. In this paper we describe the issues we uncovered, explain how the data type static analyzer of the MatlEC was implemented, explain the options we took, and suggest how the IEC 61131-3 standard could be made more explicit. © 2012 IEEE.

Abstract
This paper presents the Stacking Problem, a hard combinatorial optimization problem concerning handling and storage of items in a warehouse, where they are handled by a crane and organized into stacks. We define the problem, study its complexity class, and present a mathematical programming model to solve it. In order to tackle medium- or large-scale instances, we propose a simulation-based algorithm using semi-greedy construction heuristics. This simple approach allows for multiple constructions, finding solutions within reasonable time even for large instances. Three semi-greedy heuristics are proposed and compared in an extensive computational experiment, where we study the relation between the number of constructions and the best solution obtained using each heuristic.