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

2014-08: Generating Inductive Predicates for Symbolic Execution of Pointer-Manipulating Programs
by Thomas Ströder 26 May '14

26 May '14

The following technical report is available from http://aib.informatik.rwth-aachen.de: Generating Inductive Predicates for Symbolic Execution of Pointer-Manipulating Programs Christina Jansen, Florian Göbe, and Thomas Noll AIB 2014-08 Separation Logic (SL) is an extension of Hoare Logic that supports reasoning about pointer-manipulating programs. It employs inductively-defined predicates for specifying the (dynamic) data structures maintained at runtime, such as lists or trees. To support symbolic execution, SL introduces abstraction rules that yield symbolic representations of concrete heap states. Whenever concrete program instructions are to be applied, so-called unrolling rules are used to locally concretise the symbolic heap. To enable automatic generation of a complete set of unrolling rules, however, predicate definitions have to meet certain requirements, which are currently only implicitly specified and manually established. To tackle this problem, we exploit the relationship between SL and hyperedge replacement grammars (HRGs). The latter represent (abstracted) heaps by hypergraphs containing placeholders whose interpretation is specified by grammar rules. Earlier work has shown that the correctness of heap abstraction using HRGs requires certain structural properties, such as increasingness, which can automatically be established. We show that it is exactly the Separation Logic counterparts of those properties that enable a direct generation of abstraction and unrolling rules from predicate definitions for symbolic execution. Technically, this result is achieved by first providing formalisations of the structural properties in SL. We then extend an existing translation between SL and HRGs such that it covers all HRGs describing data structures, and show that it preserves these structural properties.

1 0

2014-07: Algorithmic Differentiation of Numerical Methods: Second-Order Tangent and Adjoint Solvers for Systems of Parametrized Nonlinear Equations
by Thomas Ströder 20 May '14

20 May '14

The following technical report is available from http://aib.informatik.rwth-aachen.de: Algorithmic Differentiation of Numerical Methods: Second-Order Tangent and Adjoint Solvers for Systems of Parametrized Nonlinear Equations Niloofar Safiran, Johannes Lotz, and Uwe Naumann AIB 2014-07 Forward and reverse modes of algorithmic differentiation (AD) transform implementations of multivariate vector functions as computer programs into tangent and adjoint code, respectively. The reapplication of the same ideas yields higher derivative code. In particular, second derivatives play an important role in nonlinear programming. Second-order methods based on Newton's algorithm promise faster convergence in the neighbourhood of the minimum by taking into account second derivative information. The adjoint mode is of particular interest in large-scale nonlinear optimization due to the independence of its computational cost on the number of free variables. Solvers for parametrized system of n equations embedded into evaluation of objective function for a (without loss of generality) unconstrained nonlinear optimization problem. Require Hessian of objective with respect to free variables implying need for second derivatives of the nonlinear solver. The local computational overhead as well as the additional memory requirement for the computation of second-order tangents/adjoints of the solution vector with respect to parameters by a fully discrete method (derived by AD) can quickly become prohibitive for large values of n. Both can be reduced extremely by the second-order continuous approach to differentiation of the underlying numerical method to be discussed in this paper.

1 0

2014-03: dco/c++ User Guide
by Thomas Ströder 12 May '14

12 May '14

The following technical report is available from http://aib.informatik.rwth-aachen.de: dco/c++ User Guide Uwe Naumann, Klaus Leppkes, and Johannes Lotz AIB 2014-03 dco/c++ is a highly flexible and efficient implementation of first- and higher-order tangent-linear and adjoint Algorithmic Differentiation (AD) by operator overloading in C++. It combines a cache-optimized internal representation based on C++ expression templates with an intuitive and powerful application programmer interface (API). Support for externally differentiated functions and for optimized data flow reversal through checkpointing is provided. dco/c++ has been applied successfully to a number of numerical simulations in the context of, for example, large-scale parameter estimation and shape optimization. Starting with an introduction to the fundamentals of AD this user guide describes the various modes of dco/c++ in terms of their APIs and with the help of very simple examples. dco/c++ is actively developed resulting in a steady evolution of the associated user guide.

1 0