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.
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.
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.
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.
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.
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.
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.
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.
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.
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.