Informatik
Refine
Year of publication
Document Type
- Preprint (817)
- Article (459)
- Working Paper (119)
- Doctoral Thesis (93)
- Diploma Thesis (47)
- Conference Proceeding (41)
- Bachelor Thesis (37)
- Book (37)
- diplomthesis (28)
- Report (25)
- Part of a Book (13)
- Contribution to a Periodical (10)
- Master's Thesis (6)
- Habilitation (1)
- Lecture (1)
- Review (1)
Has Fulltext
- yes (1735)
Is part of the Bibliography
- no (1735)
Keywords
Institute
- Informatik (1735)
- Frankfurt Institute for Advanced Studies (FIAS) (1121)
- Physik (1100)
- Mathematik (56)
- Präsidium (41)
- Medizin (25)
- Biowissenschaften (21)
- Exzellenzcluster Makromolekulare Komplexe (8)
- Psychologie (8)
- Deutsches Institut für Internationale Pädagogische Forschung (DIPF) (5)
Quarks and gluons are the building blocks of all hadronic matter, like protons and neutrons. Their interaction is described by Quantum Chromodynamics (QCD), a theory under test by large scale experiments like the Large Hadron Collider (LHC) at CERN and in the future at the Facility for Antiproton and Ion Research (FAIR) at GSI. However, perturbative methods can only be applied to QCD for high energies. Studies from first principles are possible via a discretization onto an Euclidean space-time grid. This discretization of QCD is called Lattice QCD (LQCD) and is the only ab-initio option outside of the high-energy regime. LQCD is extremely compute and memory intensive. In particular, it is by definition always bandwidth limited. Thus—despite the complexity of LQCD applications—it led to the development of several specialized compute platforms and influenced the development of others. However, in recent years General-Purpose computation on Graphics Processing Units (GPGPU) came up as a new means for parallel computing. Contrary to machines traditionally used for LQCD, graphics processing units (GPUs) are a massmarket product. This promises advantages in both the pace at which higher-performing hardware becomes available and its price. CL2QCD is an OpenCL based implementation of LQCD using Wilson fermions that was developed within this thesis. It operates on GPUs by all major vendors as well as on central processing units (CPUs). On the AMD Radeon HD 7970 it provides the fastest double-precision D= kernel for a single GPU, achieving 120GFLOPS. D=—the most compute intensive kernel in LQCD simulations—is commonly used to compare LQCD platforms. This performance is enabled by an in-depth analysis of optimization techniques for bandwidth-limited codes on GPUs. Further, analysis of the communication between GPU and CPU, as well as between multiple GPUs, enables high-performance Krylov space solvers and linear scaling to multiple GPUs within a single system. LQCD calculations require a sampling of the phase space. The hybrid Monte Carlo (HMC) algorithm performs this. For this task, a single AMD Radeon HD 7970 GPU provides four times the performance of two AMD Opteron 6220 running an optimized reference code. The same advantage is achieved in terms of energy-efficiency. In terms of normalized total cost of acquisition (TCA), GPU-based clusters match conventional large-scale LQCD systems. Contrary to those, however, they can be scaled up from a single node. Examples of large GPU-based systems are LOEWE-CSC and SANAM. On both, CL2QCD has already been used in production for LQCD studies.
Acceleration of Biomedical Image Processing and Reconstruction with FPGAs
Increasing chip sizes and better programming tools have made it possible to increase the boundaries of application acceleration with reconfigurable computer chips. In this thesis the potential of acceleration with Field Programmable Gate Arrays (FPGAs) is examined for applications that perform biomedical image processing and reconstruction. The dataflow paradigm was used to port the analysis of image data for localization microscopy and for 3D electron tomography from an imperative description towards the FPGA for the first time.
After the primitives of image processing on FPGAs are presented, a general workflow is given for analyzing imperative source code and converting it to a hardware pipeline where every node processes image data in parallel. The theoretical foundation is then used to accelerate both example applications. For localization microscopy, an acceleration of 185 compared to an Intel i5 450 CPU was achieved, and electron tomography could be sped up by a factor of 5 over an Nvidia Tesla C1060 graphics card while maintaining full accuracy in both cases.
Diese Arbeit zeigt, dass die optimale Verteilung von Individuen in Gruppen unter Beachtung ihrer Zeitpräferenzen ein NP-schweres Problem ist. Daher liegt es Nahe, dass für große Teilnehmerzahlen eine optimale Lösung nicht in praxistauglicher Zeit berechnet werden kann. Hier kann eine geeignete Heuristik Abhilfe schaffen.
Da dieses Problem in Universitäten für Studierende bei der Zuteilung der Übungsgruppen für Hunderte von Teilnehmern jedes Semester aufs Neue gelöst werden muss, macht es Sinn, dabei eine rechnergestützte Lösung einzusetzen.
In dieser Arbeit werden die gängigsten in Deutschland und insbesondere an der Goethe-Universität Frankfurt am Main verwendeten Gruppeneinteilungssysteme untersucht. Alle aktuell eingesetzten Lösungen weisen offensichtliche Mängel auf. In dieser Arbeit wird analysiert, weshalb es dazu kommt und gezeigt, wie diese Mängel vermieden werden können. Außerdem werden Kriterien entwickelt und diskutiert, die ein gutes Gruppeneinteilungssystem erfüllen sollte.
Es wird beschrieben, inwiefern eine gute mit einer Heuristik schnell berechenbare approximative Lösung des Gruppeneinteilungsproblems besser als eine perfekte Lösung sein könnte. Mehrere Heuristiken werden verglichen und eine für dieses Problem gut passende wird entwickelt und implementiert. Mithilfe der Beispielimplementierung und anhand anonymisierter Anmeldedaten für die Veranstaltungen aus vergangenen Jahren wird gezeigt, welche Ergebnisse bei dem Wechsel zu einem solchen System erreicht werden können.
Weiterhin wird analysiert, wie ein solches Gruppeneinteilungssystem an die anderen an Universitäten eingesetzten digitalen Systeme angekoppelt werden kann. Das ist notwendig, um zu vermeiden, dass die redundanten Studierendendaten doppelt gepflegt werden müssen. Somit werden Konsistenz und Korrektheit der Daten bei dem Einsatz eines neuen Systems gefördert.
Abschließend wird ein Ausblick in die Zukunft der Gruppeneinteilungssysteme gegeben und beschrieben, welche Aspekte in diesem Bereich weiterhin wichtig sein könnten.
1D-3D hybrid modeling : from multi-compartment models to full resolution models in space and time
(2014)
Investigation of cellular and network dynamics in the brain by means of modeling and simulation has evolved into a highly interdisciplinary field, that uses sophisticated modeling and simulation approaches to understand distinct areas of brain function. Depending on the underlying complexity, these models vary in their level of detail, in order to cope with the attached computational cost. Hence for large network simulations, single neurons are typically reduced to time-dependent signal processors, dismissing the spatial aspect of each cell. For single cell or networks with relatively small numbers of neurons, general purpose simulators allow for space and time-dependent simulations of electrical signal processing, based on the cable equation theory. An emerging field in Computational Neuroscience encompasses a new level of detail by incorporating the full three-dimensional morphology of cells and organelles into three-dimensional, space and time-dependent, simulations. While every approach has its advantages and limitations, such as computational cost, integrated and methods-spanning simulation approaches, depending on the network size could establish new ways to investigate the brain. In this paper we present a hybrid simulation approach, that makes use of reduced 1D-models using e.g., the NEURON simulator—which couples to fully resolved models for simulating cellular and sub-cellular dynamics, including the detailed three-dimensional morphology of neurons and organelles. In order to couple 1D- and 3D-simulations, we present a geometry-, membrane potential- and intracellular concentration mapping framework, with which graph- based morphologies, e.g., in the swc- or hoc-format, are mapped to full surface and volume representations of the neuron and computational data from 1D-simulations can be used as boundary conditions for full 3D simulations and vice versa. Thus, established models and data, based on general purpose 1D-simulators, can be directly coupled to the emerging field of fully resolved, highly detailed 3D-modeling approaches. We present the developed general framework for 1D/3D hybrid modeling and apply it to investigate electrically active neurons and their intracellular spatio-temporal calcium dynamics.
Ein Ansatz für semantisches Selbstmanagement von verteilten Anwendungen im privaten Lebensumfeld
(2014)
Die Anreicherung des privaten Lebensumfelds mit intelligenten technischen Assistenzsystemen wird in den nächsten Jahrzehnten stark zunehmen. Als Teil dieser Entwicklung wird die Nutzung von externen und hauseigenen IT-Diensten steigen, wodurch sich auch die Komplexität der entstehenden Gesamtsysteme erhöht. Hier sind Ansätze gefordert, diese Systeme auch für technisch nicht versierte Benutzer produktiv nutzbar und beherrschbar zu gestalten, um eine Überforderung zu vermeiden. Im Umfeld häuslicher Dienstplattformen, die eine zentrale Rolle in solchen Systemen übernehmen, nimmt seit ein paar Jahren die Bedeutung der semantischen Modellierung von Diensten stark zu. Diese dient zum einen der formalen Repräsentation von zugehörigen Kontextinformationen, die durch Interaktion mit Sensoren und Aktoren entstehen, und zum anderen der Verbesserung der Interoperabilität zwischen Systemen unterschiedlicher Hersteller. Bisherige Ansätze beschränken sich jedoch auf den Einsatz eines zentralen Rechenknotens zur Ausführung der Dienstplattform und nutzen Semantik – wenn überhaupt – nur zur Verarbeitung von Kontextinformationen. Ein technisches Management des Gesamtsystems findet i.d.R. nicht statt.
Vor diesem Hintergrund ist das Ziel dieser Arbeit die Entwicklung eines Ansatzes für semantisches Selbstmanagement von verteilten dienstbasierten Anwendungen speziell im Umfeld häuslicher Dienstplattformen.
Die vorliegende Arbeit definiert zunächst formale Ontologien für Dienste, Dienstgütemanagement, Selbstmanagement und zugehörige Managementregeln, die zur Laufzeit mit konkreten Diensten und deren erfassten Leistungskenngrößen integriert werden. Durch einen modellgetriebenen Architekturansatz (Model Driven Architecture, MDA) wird ein technologieunabhängiges Management auf abstrakter Ebene ermöglicht, das die Wiederverwendbarkeit von Managementregeln in anderen Szenarien erlaubt.
Dieser Ansatz wird zunächst in eine Architektur für einen hochverfügbaren autonomen Manager überführt, der die Überwachung und Steuerung von Diensten und zugehörigen Dienstplattformen übernehmen kann und auf der aus dem Autonomic Computing bekannten MAPE-K-Kontrollschleife (Monitor, Analyze, Plan, Execute, Knowledge) basiert.
Den Abschluss der Arbeit bildet eine qualitative und quantitative Evaluation (mittels einer OSGi-basierten prototypischen Umsetzung) der erreichten Ergebnisse, die einen Einsatz über die Grenzen des privaten Lebensumfelds hinaus nahelegen.
Die Simulation von Strömung in geklüftet porösen Medien ist von entscheidender Bedeutung in Hinblick auf viele hydrogeologische Anwendungsgebiete, wie beispielsweise der Vorbeugung einer Grundwasserverschmutzung in der Nähe einer Mülldeponie oder einer Endlagerstätte für radioaktive Abfälle, der Förderung fossiler Brennstoffe oder der unterirdischen Speicherung von Kohlendioxid. Aufgrund ihrer Beschaffenheit und insbesondere der großen Permeabilität innerhalb der Klüfte, stellen diese bevorzugte Transportwege dar und können das Strömungsprofil entscheidend beeinflussen. Allerdings stellt die anisotrope Geometrie der Klüfte in Zusammenhang mit den enormen Sprüngen in Parametern wie der Permeabilität auf kleinstem Raum große Anforderungen an die numerischen Verfahren.
Deswegen werden in dieser Arbeit zwei Ansätze zur Modellierung der Klüfte verfolgt. Ein niederdimensionaler Ansatz motiviert durch die anisotrope Geometrie mit sehr geringer Öffnungsweite und sehr langer Erstreckung der Klüfte und ein volldimensionaler Ansatz, der alle Vorgänge innerhalb der Kluft auflöst. Es werden die Ergebnisse dieser Ansätze für Benchmark-Probleme untersucht, mit dem Ergebnis, dass nur bei sehr dünnen Klüften der numerisch günstigere niederdimensionale Ansatz zufriedenstellende Ergebnisse liefert. Weiterhin wird ein Kriterium eingeführt, dass während der Laufzeit anhand von Eigenschaften der Kluft und Strömungsparametern angibt, ob der niederdimensionale Ansatz ausreichende Gültigkeit besitzt. Es wird ein dimensions-adaptiver Ansatz präsentiert, der dann entsprechend dieses Kriteriums einen Wechsel zum volldimensionalen Modell durchführt. Die Ergebnisse zeigen, dass so wesentlich genauere Ergebnisse erzielt werden können, ohne dass eine volle Auflösung in jedem Fall und über den gesamten Rechenzeitraum erforderlich ist.
Alternative polyadenylation (APA) is a widespread mechanism that contributes to the sophisticated dynamics of gene regulation. Approximately 50% of all protein-coding human genes harbor multiple polyadenylation (PA) sites; their selective and combinatorial use gives rise to transcript variants with differing length of their 3' untranslated region (3'UTR). Shortened variants escape UTR-mediated regulation by microRNAs (miRNAs), especially in cancer, where global 3'UTR shortening accelerates disease progression, dedifferentiation and proliferation. Here we present APADB, a database of vertebrate PA sites determined by 3' end sequencing, using massive analysis of complementary DNA ends. APADB provides (A)PA sites for coding and non-coding transcripts of human, mouse and chicken genes. For human and mouse, several tissue types, including different cancer specimens, are available. APADB records the loss of predicted miRNA binding sites and visualizes next-generation sequencing reads that support each PA site in a genome browser. The database tables can either be browsed according to organism and tissue or alternatively searched for a gene of interest. APADB is the largest database of APA in human, chicken and mouse. The stored information provides experimental evidence for thousands of PA sites and APA events. APADB combines 3' end sequencing data with prediction algorithms of miRNA binding sites, allowing to further improve prediction algorithms. Current databases lack correct information about 3'UTR lengths, especially for chicken, and APADB provides necessary information to close this gap. Database URL: http://tools.genxpro.net/apadb/
Mathematical modeling of Arabidopsis thaliana with focus on network decomposition and reduction
(2014)
Systems biology has become an important research field during the last decade. It focusses on the understanding of the systems which emit the measured data. An important part of this research field is the network analysis, investigating biological networks. An essential point of the inspection of these network models is their validation, i.e., the successful comparison of predicted properties to measured data. Here especially Petri nets have shown their usefulness as modeling technique, coming with sound analysis methods and an intuitive representation of biological network data.
A very important tool for network validation is the analysis of the Transition-invariants (TI), which represent possible steady-state pathways, and the investigation of the liveness property. The computational complexity of the determination of both, TI and liveness property, often hamper their investigation.
To investigate this issue, a metabolic network model is created. It describes the core metabolism of Arabidopsis thaliana, and it is solely based on data from the literature. The model is too complex to determine the TI and the liveness property.
Several strategies are followed to enable an analysis and validation of the network. A network decomposition is utilized in two different ways: manually, motivated by idea to preserve the integrity of biological pathways, and automatically, motivated by the idea to minimize the number of crossing edges. As a decomposition may not be preserving important properties like the coveredness, a network reduction approach is suggested, which is mathematically proven to conserve these important properties. To deal with the large amount of data coming from the TI analysis, new organizational structures are proposed. The liveness property is investigated by reducing the complexity of the calculation method and adapting it to biological networks.
The results obtained by these approaches suggest a valid network model. In conclusion, the proposed approaches and strategies can be used in combination to allow the validation and analysis of highly complex biological networks.
A concurrent implementation of software transactional memory in Concurrent Haskell using a call-by-need functional language with processes and futures is given. The description of the small-step operational semantics is precise and explicit, and employs an early abort of conflicting transactions. A proof of correctness of the implementation is given for a contextual semantics with may- and should-convergence. This implies that our implementation is a correct evaluator for an abstract specification equipped with a big-step semantics.
Towards correctness of program transformations through unification and critical pair computation
(2011)
Correctness of program transformations in extended lambda calculi with a contextual semantics is usually based on reasoning about the operational semantics which is a rewrite semantics. A successful approach to proving correctness is the combination of a context lemma with the computation of overlaps between program transformations and the reduction rules, and then of so-called complete sets of diagrams. The method is similar to the computation of critical pairs for the completion of term rewriting systems.We explore cases where the computation of these overlaps can be done in a first order way by variants of critical pair computation that use unification algorithms. As a case study we apply the method to a lambda calculus with recursive let-expressions and describe an effective unification algorithm to determine all overlaps of a set of transformations with all reduction rules. The unification algorithm employs many-sorted terms, the equational theory of left-commutativity modelling multi-sets, context variables of different kinds and a mechanism for compactly representing binding chains in recursive let-expressions.
The interactive verification system VeriFun is based on a polymorphic call-by-value functional language and on a first-order logic with initial model semantics w.r.t. constructors. It is designed to perform automatic induction proofs and can also deal with partial functions. This paper provides a reconstruction of the corresponding logic and semantics using the standard treatment of undefinedness which adapts and improves the VeriFun-logic by allowing reasoning on nonterminating expressions and functions. Equality of expressions is defined as contextual equivalence based on observing termination in all closing contexts. The reconstruction shows that several restrictions of the VeriFun framework can easily be removed, by natural generalizations: mutual recursive functions, abstractions in the data values, and formulas with arbitrary quantifier prefix can be formulated. The main results of this paper are: an extended set of deduction rules usable in VeriFun under the adapted semantics is proved to be correct, i.e. they respect the observational equivalence in all extensions of a program. We also show that certain classes of theorems are conservative under extensions, like universally quantified equations. Also other special classes of theorems are analyzed for conservativity.
The interactive verification system VeriFun is based on a polymorphic call-by-value functional language and on a first-order logic with initial model semantics w.r.t. constructors. This paper provides a reconstruction of the corresponding logic when partial functions are permitted. Typing is polymorphic for the definition of functions but monomorphic for terms in formulas. Equality of terms is defined as contextual equivalence based on observing termination in all contexts. The reconstruction also allows several generalizations of the functional language like mutual recursive functions and abstractions in the data values. The main results are: Correctness of several program transformations for all extensions of a program, which have a potential usage in a deduction system. We also proved that universally quantified equations are conservative, i.e. if a universally quantified equation is valid w.r.t. a program P, then it remains valid if the program is extended by new functions and/or new data types.
Motivated by the question of correctness of a specific implementation of concurrent buffers in the lambda calculus with futures underlying Alice ML, we prove that concurrent buffers and handled futures can correctly encode each other. Correctness means that our encodings preserve and reflect the observations of may- and must-convergence, and as a consequence also yields soundness of the encodings with respect to a contextually defined notion of program equivalence. While these translations encode blocking into queuing and waiting, we also describe an adequate encoding of buffers in a calculus without handles, which is more low-level and uses busy-waiting instead of blocking. Furthermore we demonstrate that our correctness concept applies to the whole compilation process from high-level to low-level concurrent languages, by translating the calculus with buffers, handled futures and data constructors into a small core language without those constructs.
We investigate methods and tools for analyzing translations between programming languages with respect to observational semantics. The behavior of programs is observed in terms of may- and mustconvergence in arbitrary contexts, and adequacy of translations, i.e., the reflection of program equivalence, is taken to be the fundamental correctness condition. For compositional translations we propose a notion of convergence equivalence as a means for proving adequacy. This technique avoids explicit reasoning about contexts, and is able to deal with the subtle role of typing in implementations of language extensions.
We investigate methods and tools for analyzing translations between programming languages with respect to observational semantics. The behavior of programs is observed in terms of may- and mustconvergence in arbitrary contexts, and adequacy of translations, i.e., the reflection of program equivalence, is taken to be the fundamental correctness condition. For compositional translations we propose a notion of convergence equivalence as a means for proving adequacy. This technique avoids explicit reasoning about contexts, and is able to deal with the subtle role of typing in implementations of language extensions.
We investigate methods and tools for analysing translations between programming languages with respect to observational semantics. The behaviour of programs is observed in terms of may- and mustconvergence in arbitrary contexts, and adequacy of translations, i.e., the reflection of program equivalence, is taken to be the fundamental correctness condition. For compositional translations we propose a notion of convergence equivalence as a means for proving adequacy. This technique avoids explicit reasoning about contexts, and is able to deal with the subtle role of typing in implementations of language extensions.
We investigate methods and tools for analysing translations between programming languages with respect to observational semantics. The behaviour of programs is observed in terms of may- and mustconvergence in arbitrary contexts, and adequacy of translations, i.e., the reflection of program equivalence, is taken to be the fundamental correctness condition. For compositional translations we propose a notion of convergence equivalence as a means for proving adequacy. This technique avoids explicit reasoning about contexts, and is able to deal with the subtle role of typing in implementations of language extensions.
The paper proposes a variation of simulation for checking and proving contextual equivalence in a non-deterministic call-by-need lambda-calculus with constructors, case, seq, and a letrec with cyclic dependencies. It also proposes a novel method to prove its correctness. The calculus’ semantics is based on a small-step rewrite semantics and on may-convergence. The cyclic nature of letrec bindings, as well as nondeterminism, makes known approaches to prove that simulation implies contextual equivalence, such as Howe’s proof technique, inapplicable in this setting. The basic technique for the simulation as well as the correctness proof is called pre-evaluation, which computes a set of answers for every closed expression. If simulation succeeds in finite computation depth, then it is guaranteed to show contextual preorder of expressions.