Abstract
This chapter presents a general methodology for embodying simulation as part of a tree search procedure, as a technique for solving practical problems in combinatorial optimization. Target problems are either difficult to express as mixed integer optimization models, or have models which provide rather loose bounds; in both cases, traditional, exact methods typically fail. The idea then is to have tree search instantiating part of the variables in a systematic way, and for each particular instantiation-i.e., a node in the search tree-resort to a simulation for assigning values to the remaining variables; then, use the outcome of the simulation for evaluating that node in the tree. This method has been used with considerable success in gameplaying, but has received very limited attention as a tool for optimization. Nevertheless, it has great potential, either as a way for improving known heuristics or as an alternative to metaheuristics.We depart from repeated, randomized simulation based on problem-specific heuristics for applications in scheduling, logistics, and packing, and show how the systematic search in a tree improves the results that can be obtained. © Springer International Publishing Switzerland 2015.

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
In this paper we describe a method for packing tubes and boxes in containers. Each container is divided into parts (holders) which are allocated to subsets of objects. The method consists of a recursive procedure which, based on a predefined order for dealing with tubes and boxes, determines the dimensions and position of each holder. Characteristics of the objects to pack and rules limiting their placement make this problem unique. The method devised provides timely and practical solutions.

Abstract

Abstract

Abstract
This paper presents an approaches. that assists in producing highly compacted Nesting layouts with irregular pieces using free rotations. This approach consists in the selection and compaction of big pieces in a first phase, while in a second phase, places the remaining small pieces between the big pieces, compacting all of them. The effect of several parameters are analyzed, such as minimum length to be achieved in the first phase, attraction of the pieces to the edges of the container, attraction between each pair of pieces, among others. This approach can provide good compaction results, while improving computational cost in some cases, which cart allow to tackle real world problems more effectively mkt efficiently.