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

2016-08: Derivative Code by Overloading in C++ (dco/c++): Introduction and Summary of Features
by Jera Hensel 28 Jul '17

28 Jul '17

The following technical report is available from http://aib.informatik.rwth-aachen.de: <http://aib.informatik.rwth-aachen.de/> Derivative Code by Overloading in C++ (dco/c++): Introduction and Summary of Features Klaus Leppkes, Johannes Lotz, and Uwe Naumann AIB 2016-08 dco/c++ is a flexible and efficient implementation of first- and higher-order tangent 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. It also has bindings in Fortran and MATLAB. dco/c++ has been applied successfully to a number of numerical simulations in the context of, for example, large-scale parameter estimation, shape optimization, or computational finance. dco/c++ is under active development. This report provides a basic reference in form of a brief introduction to derivative code resulting from the application of AD to numerical simulation programs, a description of the four fundamental differentiation modes (first- and second-order tangent and adjoint modes, respectively) and a list of all features of the current version of dco/c++. An in-depth discussion of the latter is beyond this document. Further information on the tool can be obtained by contacting info(a)stce.rwth-aachen.de.

1 0

2017-06: CD2Alloy: A Translation of Class Diagrams to Alloy
by Hensel, Jera 03 Jul '17

03 Jul '17

The following technical report is available from http://aib.informatik.rwth-aachen.de: CD2Alloy: A Translation of Class Diagrams to Alloy Oliver Kautz, Shahar Maoz, Jan Oliver Ringert, and Bernhard Rumpe AIB 2017-06 This report presents a translation from UML class diagrams [OMG15, Rum16] to Alloy modules [Jac06] and a translation from Alloy instances back to UML object diagrams. An overview of the translation was first presented in [MRR11a] and applied in [MRR11b] to semantic differencing of class diagrams. It supports an extended list of CD language features, including, e.g., directed associations, composite aggregations, interfaces, multiple inheritance, and enumerations. The translation thus supports essential features of many real-world CDs, UML and EMF metamodels, practically not analyzable before. An important feature of the translation is the ability to analyze multiple class diagrams within one Alloy module, which is not possible with previous translations. This document defines the translations by translation rules that operate on the abstract syntax of a class diagram language and produce concrete syntax of the Alloy language. We give examples showing class diagrams and complete representations in Alloy as well as an Alloy instance and its object diagram representation.

1 0

2017-05: Complexity Analysis for Term Rewriting by Integer Transition Systems
by Hensel, Jera 03 Jul '17

03 Jul '17

The following technical report is available from http://aib.informatik.rwth-aachen.de: Complexity Analysis for Term Rewriting by Integer Transition Systems Matthias Naaf, Florian Frohn, Marc Brockschmidt, Carsten Fuhs, and Jürgen Giesl AIB 2017-05 We present a new method to infer upper bounds on the innermost runtime complexity of term rewrite systems (TRSs), which benefits from recent advances on complexity analysis of integer transition systems (ITSs). To this end, we develop a transformation from TRSs to a generalized notion of ITSs with (possibly non-tail) recursion. To analyze their complexity, we introduce a modular technique which allows us to use existing tools for standard ITSs in order to infer complexity bounds for our generalized ITSs. The key idea of our technique is a summarization method that allows us to analyze components of the transition system independently. We implemented our contributions in the tool AProVE, and our experiments show that one can now infer bounds for significantly more TRSs than with previous state-of-the-art tools for term rewriting.

1 0

2017-04: Complexity Analysis for Java with AProVE
by Hensel, Jera 03 Jul '17

03 Jul '17

The following technical report is available from http://aib.informatik.rwth-aachen.de: Complexity Analysis for Java with AProVE Florian Frohn and Jürgen Giesl AIB 2017-04 While AProVE is one of the most powerful tools for termination analysis of Java since many years, we now extend our approach in order to analyze the complexity of Java programs as well. Based on a symbolic execution of the program, we develop a novel transformation of (possibly heap-manipulating) Java programs to integer transition systems (ITSs). This allows us to use existing complexity analyzers for ITSs to infer runtime bounds for Java programs. We demonstrate the power of our implementation on an established standard benchmark set.

1 0