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