- tr-announce - lists.rwth-aachen.de

2011-24: Demonstration of a Branch-and-Bound Algorithm for Global Optimization using McCormick Relaxations
by Carsten Fuhs 27 Nov '11

27 Nov '11

The following technical report is available from http://aib.informatik.rwth-aachen.de: Demonstration of a Branch-and-Bound Algorithm for Global Optimization using McCormick Relaxations Callum Corbett, Uwe Naumann, Alexander Mitsos AIB 2011-24 This report is meant to demonstrate the actions performed by a branch-and-bound algorithm for global optimization on a simple minimization problem. McCormick relaxations are used to construct piecewise affine underestimators of the objective function.

1 0

2011-10: Adjoint Subgradient Calculation for McCormick Relaxations
by Carsten Fuhs 12 Oct '11

12 Oct '11

The following technical report is available from http://aib.informatik.rwth-aachen.de: Adjoint Subgradient Calculation for McCormick Relaxations Markus Beckers, Viktor Mosenkis, Michael Maier, Uwe Naumann AIB 2011-10 In [Corbett 2010] the library modMC was presented which allows the propagation of McCormick relaxations and their corresponding subgradients based on the forward mode of Algorithmic Differentiation (AD). Subgradients are natural extensions of usual derivatives which allow the application of derivative based methods on possibly nondifferentiable convex and concave functions. These subgradients can be computed by AD, a method which allows the computation of derivatives with machine accuracy even for highly complex functions implemented by a computer program. In this article we present the advancement of modMC by reverse mode AD. Reverse mode AD is an adjoint method for the propagation of derivatives which is preferable when scalar functions are considered. We describe the theory behind the application of reverse mode in subgradient propagation as well as the improved library amodMC in detail. The calculated subgradients are used in an deterministic global optimization algorithm which is based on a branch-and-bound method. The improvements gained using Reverse instead of Forward mode AD are illustrated by several examples.

1 0

2011-09: Fifth SIAM Workshop on Combinatorial Scientific Computing
by Carsten Fuhs 12 Oct '11

12 Oct '11

The following technical report is available from http://aib.informatik.rwth-aachen.de: Fifth SIAM Workshop on Combinatorial Scientific Computing Markus Beckers, Johannes Lotz, Viktor Mosenkis, Uwe Naumann (Editors) AIB 2011-09 The human desire for meaningful numerical simulation of physical, chemical, and biological phenomena in science and engineering has been increasing with the growing performance of the continuously improving computer systems. As a result of this development, we are (and will always be) faced with a large (and growing) number of highly complex numerical simulation codes that run at the limit of the available high-performance computing resources. These codes often result from the discretization of systems of differential equations. The runtime correlates with the resolution that often needs to be very high in order to capture the real behavior of the underlying system. There is no doubt that the available hardware will always be used to the extreme. Improvements in the runtime of the simulations need to be sought through research in numerical algorithms and their efficient implementation on parallel architectures. Many of the resulting problems are combinatorial in nature. Most of those are known to be computationally hard in the sense that efficient (polynomial in the required time and memory space) algorithms for their exact solution are unlikely to exist. For example, we have to deal with partitioning, elimination ordering, coloring, and matching problems for graphs and hypergraphs in various contexts. A good approximation of the solution to these abstract problems may lead to a significant decrease in the runtime of numerical programs that implement solvers for partial differential equations, nonlinear optimization algorithms, or solvers for generalized Eigenvalue problems. Problem sizes are typically now in the millions of unknowns; and with emerging large-scale computing systems, this size is expected to increase by a factor of thousand over the next five years. Moreover, simulations are increasingly used in design optimization and parameter identification which is even more complex and requires the highest possible computational performance and fundamental enabling algorithmic technology. What binds together the community of combinatorial scientific computing is the focus on practical use of graph algorithms and combinatorial algorithms to address a variety of different problems that all arise in scientific computing. This shared common denominator allows us to interact productively and to advance the state of the art in several different problem areas. The Fifth SIAM Workshop on Combinatorial Scientific Computing represents another important milestone. Three CSC experts have been invited to present plenary talks on various important aspects of CSC: Thomas F. Coleman (University of Waterloo, Canada): Efficient Automatic Differentiation for Nonlinear Systems and Continuous Optimization (by using graphs) Burkhard Monien (Paderborn University, Germany): Recent Trends in Graph Partitioning for Scientific Computing Trond Steihaug (Bergen University, Norway): Sparse Matrix Structures and Higher Derivatives This collection of extended abstracts covers all accepted contributed oral and poster presentations. It is meant to give both participants of CSC11 and other interested readers an overview of recent results and ongoing research and development projects in the area of Combinatorial Scientific Computing.

1 0

2011-19: Automated Detection of Non-Termination and NullPointerExceptions for Java Bytecode
by Carsten Fuhs 12 Sep '11

12 Sep '11

The following technical report is available from http://aib.informatik.rwth-aachen.de: Automated Detection of Non-Termination and NullPointerExceptions for Java Bytecode Marc Brockschmidt, Thomas Ströder, Carsten Otto, Jürgen Giesl AIB 2011-19 Recently, we developed an approach for automated termination proofs of Java Bytecode (JBC), which is based on constructing and analyzing termination graphs. These graphs represent all possible program executions in a finite way. In this paper, we show that this approach can also be used to detect non-termination or NullPointerExceptions. Our approach automatically generates witnesses, i.e., calling the program with these witness arguments indeed leads to non-termination resp. to a NullPointerException. Thus, we never obtain "false positives". We implemented our results in the termination prover AProVE and provide experimental evidence for the power of our approach.

1 0

2011-12: On Compositional Failure Detection in Structured Transition Systems
by Carsten Fuhs 19 Aug '11

19 Aug '11

The following technical report is available from http://aib.informatik.rwth-aachen.de: On Compositional Failure Detection in Structured Transition Systems Ingo Felscher, Wolfgang Thomas AIB 2011-12 In model-checking, systems are often given as products. We propose an approach that is built on a preprocessing of specifications in terms of appropriate automata. This allows to incorporate information about the local behaviour and synchronization of the system components into the specification. We develop a framework of (partially) synchronized automaton products and a format of corresponding specification automata that allows for a compositional failure detection of linear regular properties (either for finite or for infinite behaviour). As a result we obtain an algorithm which separates the local and the non-local segments of system runs, resulting in improved complexity bounds in typical specifications.

1 0

2011-18: Introducing Timers to pi-Calculus
by Carsten Fuhs 16 Aug '11

16 Aug '11

The following technical report is available from http://aib.informatik.rwth-aachen.de: Introducing Timers to pi-Calculus Kamal Barakat AIB 2011-18 Modeling systems of concurrent processes can be improved if the concept of time is represented in the model. Pi-calculus is a suitable process algebra for modeling communicating processes that exchange messages and is able to model mobility through dynamic channel setup and through privatizing names using restriction. Therefore, it is beneficial to extend pi-calculus to embrace the notion of time.

1 0

2011-16: Toward Adjoint OpenFOAM
by Carsten Fuhs 27 Jul '11

27 Jul '11

The following technical report is available from http://aib.informatik.rwth-aachen.de: Toward Adjoint OpenFOAM Niloofar Safiran, Uwe Naumann AIB 2011-16 OpenFOAM is a package which simplifies the implementation of physical models by mimicking the form of partial differential equations in software. Use of OpenFOAM is rapidly expanding in the research community and among industrial users, covering a wide range of continuum models. AD provides accurate derivative values and better runtime performance of the adjoint model compared with finite differences. This paper presents a transformation of the OpenFOAM code that can be used for calculating derivatives with adjoint mode of AD. An example based on ODE is considered here.

1 0

2011-14: Solving Muller Games via Safety Games
by Carsten Fuhs 20 Jul '11

20 Jul '11

The following technical report is available from http://aib.informatik.rwth-aachen.de: Solving Muller Games via Safety Games Daniel Neider, Roman Rabinovich, Martin Zimmermann AIB 2011-14 We show how to transform a Muller game with n vertices into a safety game with (n!)^3 vertices whose solution allows to determine the winning regions of the Muller game and a winning strategy for one player.

1 0

2011-07: An Operational Semantics for Activity Diagrams using SMV
by Carsten Fuhs 13 Jul '11

13 Jul '11

The following technical report is available from http://aib.informatik.rwth-aachen.de: An Operational Semantics for Activity Diagrams using SMV Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe AIB 2011-07 This document defines an operational semantics for activity diagrams (ADs) using a translation to SMV. The translation is inspired by the work of Eshuis [Esh06] and extends it with support for data. Each execution step of the SMV module obtained from an AD represents an executed action of this AD with interleaved execution of concurrent branches. An implementation of the given translation was used in the context of semantic differencing for ADs [MRR11]. We define the translation and give two examples, showing ADs and their complete representation in SMV.

1 0

2011-13: Toward Adjoint OpenMP
by Carsten Fuhs 08 Jul '11

08 Jul '11

The following technical report is available from http://aib.informatik.rwth-aachen.de: Toward Adjoint OpenMP Michael Förster, Uwe Naumann, Jean Utke AIB 2011-13 Shared-memory multiprocessing is becoming increasingly important in high-performance scientific computing. Algorithmic differentiation provides accurate derivative values and better runtime performance of the adjoint model compared with finite differences. This paper presents a source-to-source transformation of OpenMP augmented code that can be used in source transformation tools for creating the adjoint code of a given input code. Only some directives of the OpenMP standard are considered here, namely, directives to parallelize loops.

1 0