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

2013-06: Better termination proving through cooperation
by Thomas Ströder 14 Apr '13

14 Apr '13

The following technical report is available from http://aib.informatik.rwth-aachen.de: Better termination proving through cooperation Marc Brockschmidt, Byron Cook, and Carsten Fuhs AIB 2013-06 One of the difficulties of proving program termination is managing the subtle interplay between the finding of a termination argument and the finding of the argument's supporting invariant. In this paper we propose a new mechanism that facilitates better cooperation between these two types of reasoning. In an experimental evaluation we find that our new method leads to dramatic performance improvements.

1 0

2013-05: Software & Systems Engineering Essentials 2013
by Thomas Ströder 13 Mar '13

13 Mar '13

The following technical report is available from http://aib.informatik.rwth-aachen.de: Software & Systems Engineering Essentials 2013 Andreas Rausch and Marc Sihling AIB 2013-05 Software verändert unseren Alltag deutlich und nachhaltig. In der neuen IT-Welt installieren und nutzen auch technisch kaum versierte Anwender wie selbstverständlich Software auf mobilen Geräten - vom Smartphone über ihr Tablet bis hin zum Bordcomputer ihres Autos. Es ist einfacher denn je, Softwarelösungen auszuprobieren, up-to-date zu halten und bei Nicht-Gefallen wieder zu entfernen. Software wird damit zum Motor der Veränderung für Wirtschaft und Gesellschaft. Die Konferenz SEE2013 fand vom 27. Februar bis 1. März in Aachen im Rahmen der Multikonferenz SE2013 statt. Den Besuchern wurden parallel zu den Beiträgen der SE2013 16 Vorträge aus Industrie und Wirtschaft angeboten. Die Multikonferenz wurde von einer Ausstellung mit Vertretern von Werkzeugherstellern, Industriekunden und Beratungsfirmen begleitet.

1 0

2013-04: Algorithmic Differentiation of a Complex C++ Code with Underlying Libraries
by Thomas Ströder 05 Mar '13

05 Mar '13

The following technical report is available from http://aib.informatik.rwth-aachen.de: Algorithmic Differentiation of a Complex C++ Code with Underlying Libraries Max Sagebaum, Nicolas R. Gauger, Uwe Naumann, Johannes Lotz, and Klaus Leppkes AIB 2013-04 Algorithmic differentiation (AD) is a mathematical concept which evolved over the last decades to a very robust and well understood tool for computation of derivatives. It can be applied to mathematical algorithms, codes for numerical simulation, and whenever derivatives are needed. In this paper we report on the algorithmic differentiation of the discontinuous Galerkin solver padge, a large and complex code written in C++ with underlying external libraries. The reports on successful application of AD to large scale codes are rare in literature and up to now this is not state of the art. Most of the codes, which are differentiated nowadays, are written in C or Fortran. The padge code was differentiated with the operator overloading tool dco/c++ in forward as well as reverse mode. The differentiated code is validated and runs in the expected time margins of AD.

1 0

2013-03: A Discrete Adjoint Model for OpenFOAM
by Thomas Ströder 13 Feb '13

13 Feb '13

The following technical report is available from http://aib.informatik.rwth-aachen.de: A Discrete Adjoint Model for OpenFOAM Markus Towara and Uwe Naumann AIB 2013-03 We present a discrete adjoint version of OpenFOAM obtained by operator overloading which yields, in comparison to continuous adjoint versions, a greater flexibility and robustness. We discuss our implementation and how the discrete adjoint version of OpenFOAM differs from existing continuous implementations. To reduce the inherent memory requirement of discrete adjoint code we introduce a checkpointing scheme to trade computation time for memory. Moreover we show results from a relevant reference case.

1 0

2012-16: SMC-MuSe: A Framework for Secure Multi-Party Computation on MultiSets
by Thomas Ströder 05 Dec '12

05 Dec '12

The following technical report is available from http://aib.informatik.rwth-aachen.de: SMC-MuSe: A Framework for Secure Multi-Party Computation on MultiSets Georg Neugebauer and Ulrike Meyer AIB 2012-16 Secure Multi-Party Computation (SMC) offers a theoretically well-founded way to enable applications that preserve their users' privacy. However, the practical use of SMC has often been questioned in the past. This is partly due to the fact that the system assumptions made in theory are hard to meet in practice and partly due to the potentially very high overhead general purpose SMC frameworks induce on clients. In this report, we aim at bringing SMC closer to regular Internet users. We introduce SMC-MuSe, a framework for Secure Multi-Party Computation on MultiSets. SMC-MuSe is targeted at the efficient implementation of specific interesting functions rather then on computing arbitrary ones. It is generic in the sense that it allows to compute any composition of privacy-preserving set intersections, unions, and reductions on multisets. The system model used in SMC-MuSe is kept close to the one assumed in theory and supports asynchronous communications, resilient SMC computations, and fully automated key management.

1 0

2012-15: Algorithmic Differentiation of Numerical Methods: Tangent-Linear and Adjoint Solvers for Systems of Nonlinear Equations
by Thomas Ströder 12 Oct '12

12 Oct '12

The following technical report is available from http://aib.informatik.rwth-aachen.de: Algorithmic Differentiation of Numerical Methods: Tangent-Linear and Adjoint Solvers for Systems of Nonlinear Equations Uwe Naumann, Johannes Lotz, Klaus Leppkes, and Markus Towara AIB 2012-15 We consider the Algorithmic Differentiation (also know as Automatic Differentiation; AD) of numerical simulation programs which contain calls to solvers for parameterized systems of n nonlinear equations. The local computational overhead as well as the additional memory requirement for the computation of directional derivatives or adjoints of the solution vector with respect to the parameters can quickly become prohibitive for large values of n. Both can be reduced drastically by the semi-discrete and continuous approaches to differentiation of the underlying numerical method to be discussed in this paper.

1 0

2011-17: SAT Encodings: From Constraint-Based Termination Analysis to Circuit Synthesis
by Thomas Ströder 02 Oct '12

02 Oct '12

The following technical report is available from http://aib.informatik.rwth-aachen.de: SAT Encodings: From Constraint-Based Termination Analysis to Circuit Synthesis Carsten Fuhs AIB 2011-17 Termination is one of the most prominent undecidable problems in computer science. At the same time, the problem whether a given program terminates for all inputs is sufficiently important for the area of program verification to spur decades-long efforts in developing sufficient criteria for concluding termination. In the last decade, the focus of this research has been on automation, giving rise to several powerful fully automatic termination provers. However, the search problems that arise during the synthesis of a successful termination proof are typically NP-complete. To tackle these algorithmic challenges, over the last years a two-stage process has turned out to be extremely successful in practice: First encode the arising problem instance to the satisfiability problem of propositional logic (SAT), and then invoke a state-of-the-art SAT solver on this SAT instance. The solution found by the SAT solver is then used in the termination proof. While in the worst case still prohibitive due to NP-completeness of SAT, this approach has increased performance on practical problem instances for existing termination techniques by orders of magnitude. At the same time, the approach has also made new automated techniques possible that were out of reach before. This thesis contributes efficient SAT-based automation both for several existing termination techniques and also for new techniques that we have developed in the dependency pair framework for termination analysis of term rewriting. The usefulness of SAT encodings goes beyond the field of termination analysis. We have transferred the approach used for termination techniques to the - at first glance - quite distinct application domain of circuit synthesis, allowing us to obtain a provably optimal implementation of a part of the Advanced Encryption Standard. The contributions of this thesis are implemented within our fully automated termination prover AProVE. The significance of our results is demonstrated also by AProVE reaching the highest scores in the annual International Termination Competitions of 2007 - 2011. At these competitions, the leading automated termination analysis tools try to prove or disprove termination of programs originating from various areas of computer science.

1 0

2012-10: Algorithmic Differentiation of Numerical Methods: Tangent-Linear and Adjoint Direct Solvers for Systems of Linear Equations
by Thomas Ströder 05 Jul '12

05 Jul '12

The following technical report is available from http://aib.informatik.rwth-aachen.de: Algorithmic Differentiation of Numerical Methods: Tangent-Linear and Adjoint Direct Solvers for Systems of Linear Equations Uwe Naumann and Johannes Lotz AIB 2012-10 We consider the Algorithmic Differentiation (also know as Automatic Differentiation; AD) of numerical simulation programs that contain calls to direct solvers for systems of n linear equations. AD of the linear solvers yields a local overhead of O(n^3) for the computation of directional derivatives or adjoints of the solution vector with respect to the system matrix and right-hand side. The local memory requirement is of the same order in adjoint mode AD. Mathematical insight yields a reduction of the local computational complexity to O(n^2). The memory overhead can be reduced to at least O(n^2) in adjoint mode. We derive efficient tangent-linear and adjoint direct linear solvers and illustrate their use within tangent-linear and adjoint versions of the enclosing numerical simulation.

1 0

2012-12: Symbolic Evaluation Graphs and Term Rewriting --- A General Methodology for Analyzing Logic Programs
by Thomas Ströder 29 Jun '12

29 Jun '12

The following technical report is available from http://aib.informatik.rwth-aachen.de: Symbolic Evaluation Graphs and Term Rewriting --- A General Methodology for Analyzing Logic Programs Jürgen Giesl, Thomas Ströder, Peter Schneider-Kamp, Fabian Emmes, and Carsten Fuhs AIB 2012-12 There exist many powerful techniques to analyze termination and complexity of term rewrite systems (TRSs). Our goal is to use these techniques for the analysis of other programming languages as well. For instance, approaches to prove termination of definite logic programs by a transformation to TRSs have been studied for decades. However, a challenge is to handle languages with more complex evaluation strategies (such as Prolog, where predicates like the cut influence the control flow). In this paper, we present a general methodology for the analysis of such programs. Here, the logic program is first transformed into a symbolic evaluation graph which represents all possible evaluations in a finite way. Afterwards, different analyses can be performed on these graphs. In particular, one can generate TRSs from such graphs and apply existing tools for termination or complexity analysis of TRSs to infer information on the termination or complexity of the original logic program.

1 0

2012-09: Quantitative Timed Analysis of Interactive Markov Chains
by Thomas Ströder 29 Jun '12

29 Jun '12

The following technical report is available from http://aib.informatik.rwth-aachen.de: Quantitative Timed Analysis of Interactive Markov Chains Dennis Guck, Tingting Han, Joost-Pieter Katoen, and Martin R. Neuhäußer AIB 2012-09 This paper presents new algorithms and accompanying tool support for analyzing interactive Markov chains (IMCs), a stochastic timed 1 1/2-player game in which delays are exponentially distributed. IMCs are compositional and act as semantic model for engineering formalisms such as AADL and dynamic fault trees. We provide algorithms for determining the extremal expected time of reaching a set of states, and the long-run average of time spent in a set of states. The prototypical tool Imca supports these algorithms as well as the synthesis of ε-optimal piecewise constant timed policies for timed reachability objectives. Two case studies show the feasibility and scalability of the algorithms.

1 0