tr-announce

Download

tr-announce@lists.rwth-aachen.de

October 2012

1 participants
2 discussions

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