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
This paper proposes a method for computing the expectation for the length of a maximum set of vertex-disjoint cycles in a digraph where vertices and/or arcs are subject to failure with a known probability. This method has an immediate practical application: it can be used for the solution of a kidney exchange program in the common situation where the underlying graph is unreliable. Results for realistic benchmark instances are reported and analyzed.

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
In the literature, the most widely referred approaches regarding forest harvesting scheduling problems involving environmental concerns have typically addressed constraints on the maximum clear-cut area. Nevertheless, the solutions arising from those approaches in general display a loss of habitat availability. Such loss endangers the survival of many wild species. This study presents a branch-and-bound procedure designed to find good feasible solutions, in a reasonable time, to forest harvest scheduling problems with constraints on the clear-cut area and habitat availability. Two measures are applied for the habitat availability constraints: the area of all habitats and the connectivity between them. In each branch of the branch-and-bound tree, a partial solution leads to two children nodes, corresponding to the cases of harvesting or not harvesting a given stand in a given period. Pruning is based on constraint violations or unreachable objective values. Computational results are reported.

Abstract
SCIP is a solver for a wide variety of mathematical optimization problems. It is written in C and extendable due to its plug-in based design. However, dealing with all C specifics when extending SCIP can be detrimental to development and testing of new ideas. This paper attempts to provide a remedy by introducing PySCIPOPT, a Python interface to SCIP that enables users to write new SCIP code entirely in Python. We demonstrate how to intuitively model mixed-integer linear and quadratic optimization problems and moreover provide examples on how new Python plug-ins can be added to SCIP.

Abstract