### Refine

#### Year of publication

#### Document Type

- Doctoral Thesis (139) (remove)

#### Language

- English (139) (remove)

#### Keywords

- Visualisierung (13)
- Computergraphik (5)
- Visualization (5)
- Evaluation (3)
- Geoinformationssystem (3)
- Mustererkennung (3)
- Ray casting (3)
- Robotik (3)
- Scientific Visualization (3)
- Semantic Web (3)
- computer graphics (3)
- document analysis (3)
- optical character recognition (3)
- verification (3)
- visualization (3)
- Algorithmus (2)
- Bildverarbeitung (2)
- Computational Fluid Dynamics (2)
- Datenanalyse (2)
- Datenbank (2)
- Endlicher Automat (2)
- Layout (2)
- Merkmalsextraktion (2)
- Model Checking (2)
- Optische Zeichenerkennung (2)
- Raumakustik (2)
- Recommender Systems (2)
- Room acoustics (2)
- Scattered-Data-Interpolation (2)
- Topology (2)
- Uncertainty Visualization (2)
- image processing (2)
- layout analysis (2)
- machine learning (2)
- virtual acoustics (2)
- 3D Gene Expression (1)
- 3D Point Data (1)
- ASM (1)
- AUTOSAR (1)
- Ableitungsschätzung (1)
- Abrechnungsmanagement (1)
- Abstraction (1)
- Abstraktion (1)
- Accounting Agent (1)
- Activity Recognition, Wearable Computing, Minimal Training, Unobtrusive Instrumentations (1)
- Activity recognition (1)
- Adaptive Data Structure (1)
- Affine Arithmetic (1)
- Algorithm (1)
- Algorithmic Differentiation (1)
- Application Framework (1)
- Artificial Intelligence (1)
- Association (1)
- Automat <Automatentheorie> (1)
- Automatische Differentiation (1)
- Automatisches Beweisverfahren (1)
- Autonomer Roboter (1)
- Befahrbarkeitsanalyse (1)
- Benutzer (1)
- Beschränkte Arithmetik (1)
- Bioinformatik (1)
- Bluetooth (1)
- Boosting (1)
- Caching (1)
- Carbon footprint (1)
- Classification (1)
- Cluster-Analyse (1)
- Code Generation (1)
- Collaboration (1)
- Combinatorial Testing (1)
- Computer Graphic (1)
- Computer Supported Cooperative Work (1)
- Computer graphics (1)
- Computerphysik (1)
- Computersimulation (1)
- Computertomographie (1)
- Computervision (1)
- Cycle Accuracy (1)
- DCE <Programm> (1)
- DFG (1)
- DPN (1)
- Data Modeling (1)
- Dataset (1)
- Decision Support Systems (1)
- Delaunay-Triangulierung (1)
- Derivative Estimation (1)
- Direct Numerical Simulation (1)
- Discrete Event Simulation (DES) (1)
- Distributed Rendering (1)
- Distributed system (1)
- Dreidimensionale Bildverarbeitung (1)
- Dreidimensionale Rekonstruktion (1)
- Dreidimensionale Strömung (1)
- Duplicate Identification (1)
- Duplikaterkennung (1)
- Effizienter Algorithmus (1)
- Empfehlungssysteme (1)
- Ensemble Visualization (1)
- Entwurf (1)
- Evolutionary Algorithm (1)
- Experiment (1)
- Experimentation (1)
- Extrapolation (1)
- Fahrtkostenmodelle (1)
- Fault Tree Analysis (1)
- Feasibility study (1)
- Feature (1)
- Feature Detection (1)
- Feature Extraction (1)
- Fehlerbaumanalyse (1)
- Fließanalyse (1)
- Flow Visualization (1)
- Formale Grammatik (1)
- Formale Sprache (1)
- Formaler Beweis (1)
- Framework (1)
- Functional Safety (1)
- Funktionale Sicherheit (1)
- Fusion (1)
- Future Internet (1)
- GPU (1)
- Gateway (1)
- Gauß-Filter (1)
- Gefahren- und Risikoanalyse (1)
- Gene expression programming (1)
- Generierung (1)
- Geovisualization (1)
- Google Earth (1)
- HPC (1)
- Hazard Analysis (1)
- Heterogeneous (1)
- Hitting families (1)
- Hypergraph (1)
- IEEE 802.15.4 (1)
- IP Address (1)
- IP Traffic Accounting (1)
- IP-XACT (1)
- ISO 26262 (1)
- Image Processing (1)
- Implementierung (1)
- Incremental recomputation (1)
- Induktive logische Programmierung (1)
- Information Extraction (1)
- Information Visualization (1)
- Intensity estimation (1)
- Interaction (1)
- Interaktion (1)
- Intermediate Composition (1)
- Interpolation (1)
- Invariante (1)
- Invariante Momente (1)
- Kellerautomat (1)
- Klassifikation (1)
- Knowledge Management (1)
- Knuth-Bendix completion (1)
- Knuth-Bendix-Vervollständigung (1)
- Kompression (1)
- Korrelationsanalyse (1)
- Kurve (1)
- LIDAR (1)
- LIR-Tree (1)
- Large High-Resolution Displays (1)
- Laser Wakefield Particle Accelerator (1)
- Leistungsmessung (1)
- Linked Data (1)
- Linking Data Analysis and Visualization (1)
- Lokalisierung (1)
- Lärmbelastung (1)
- Lärmimmission (1)
- MAC protocols (1)
- MIP-Emissionsspektroskopie (1)
- MIP-Massenspektrometrie (1)
- Machine Learning (1)
- Machine learning (1)
- Magnetfeldbasierter Lokalisierung (1)
- Magnetfelder (1)
- Manufacturing (1)
- MapReduce (1)
- Maschinelle Übersetzung (1)
- Maximum Intensity Projection (1)
- Memory Architecture (1)
- Memory Consistency (1)
- Mensch-Maschine-Kommunikation (1)
- Menschenmenge (1)
- Merkmalsraum (1)
- Mesh-Free (1)
- Meter (1)
- Mikroskopie (1)
- Minimal Cut Set Visualization (1)
- Mobile system (1)
- Mobiler Roboter (1)
- Modellierung (1)
- Modularisierung (1)
- Molekulare Bioinformatik (1)
- Moment Invariants (1)
- Mood-based Music Recommendations (1)
- Multi-Edge Graph (1)
- Multi-Field (1)
- Multi-Variate Data (1)
- Multifield Data (1)
- Nachhaltigkeit (1)
- Natural Language Processing (1)
- Natural Neighbor (1)
- Natural Neighbor Interpolation (1)
- Natürliche Nachbarn (1)
- Navigation (1)
- Network Architecture (1)
- Network Calculus (1)
- Netzwerk (1)
- Node-Link Diagram (1)
- Numerische Strömungssimulation (1)
- OCR (1)
- Off-road Robotics (1)
- Off-road Robotik (1)
- Online chain partitioning (1)
- Optimierender Compiler (1)
- Optimierung (1)
- Paralleler Hybrid (1)
- Pareto Optimality (1)
- Partial Differential Equations (1)
- Partially ordered sets (1)
- Participatory Sensing (1)
- Pattern Recognition (1)
- Performance (1)
- Personalisation (1)
- Pervasive health (1)
- Physical activity monitoring (1)
- Planar Pressure (1)
- Process Data (1)
- Processor Architecture (1)
- Protocol Composition (1)
- Prototyp (1)
- Prototype (1)
- Prozessvisualisierung (1)
- Quantitative Bildanalyse (1)
- Quartz (1)
- Quicksort (1)
- Random testing (1)
- Ray tracing (1)
- Rechtecksgitter (1)
- Rectilinear Grid (1)
- Redundanzvermeidung (1)
- Representation (1)
- Risikobewertung (1)
- Risk Assessment (1)
- Roboter (1)
- Räumliche Statistik (1)
- SAHARA (1)
- SDL (1)
- SDL extensions (1)
- SPARQL (1)
- SPARQL query learning (1)
- Safety Analysis (1)
- Scalar (1)
- Schema <Informatik> (1)
- Schematisation (1)
- Schematisierung (1)
- Semantic Wikis (1)
- Semantische Modellierung (1)
- Semantisches Datenmodell (1)
- Sensing (1)
- Shared Resource Modeling (1)
- Sicherheitsanalyse (1)
- Similarity Join (1)
- Similarity Joins (1)
- Simulation (1)
- Skalar (1)
- Smart City (1)
- Smart Textile (1)
- Smartphone (1)
- Smartwatch (1)
- Socio-Semantic Web (1)
- Software Comprehension (1)
- Software Dependencies (1)
- Software Evolution (1)
- Software Maintenance (1)
- Software Measurement (1)
- Software Testing (1)
- Software Visualization (1)
- Software engineering (1)
- Software-Architektur (1)
- Softwareentwicklung (1)
- Softwaremetrie (1)
- Softwarewartung (1)
- Sprachdefinition (1)
- Sprachprofile (1)
- Stimmungsbasierte Musikempfehlungen (1)
- Stokes Equations (1)
- Streaming (1)
- Strukturiertes Gitter (1)
- Strömung (1)
- Surface Reconstruction (1)
- SystemC (1)
- Systemarchitektur (1)
- Systemdesign (1)
- Task-based (1)
- Temporal Decoupling (1)
- Temporal data processing (1)
- Tensor (1)
- Tensorfeld (1)
- Tesselation (1)
- Tetraeder (1)
- Tetraedergi (1)
- Tetrahedral Grid (1)
- Tetrahedral Mesh (1)
- Themenbasierte Empfehlungen von Ressourcen (1)
- Topic-based Resource Recommendations (1)
- Topologie (1)
- Topology visualization (1)
- Transaction Level Modeling (TLM) (1)
- Transport Protocol (1)
- Traversability Analysis (1)
- UML (1)
- Ubiquitous system (1)
- Unorganized Data (1)
- Unstrukturiertes Gitter (1)
- Urban sprawl (1)
- UrbanSim (1)
- User Model (1)
- Validierung (1)
- Vector (1)
- Vector Field (1)
- Vektor (1)
- Vektorfelder (1)
- Verifikation (1)
- Verzerrungstensor (1)
- Visual Analytics (1)
- Visual Queries (1)
- Volume rendering (1)
- Volumen-Rendering (1)
- Voronoi diagram (1)
- Voronoi-Diagramm (1)
- Weak Memory Model (1)
- Wearable computing (1)
- WiFi (1)
- Wide-column stores (1)
- XDBMS (1)
- XML (1)
- XML query estimation (1)
- XML summary (1)
- Yaroslavskiy-Bentley-Bloch Quicksort (1)
- acoustic modeling (1)
- affective user interface (1)
- affine arithmetic (1)
- analysis of algorithms (1)
- artificial intelligence (1)
- artificial neural network (1)
- associations (1)
- automated theorem proving (1)
- average-case analysis (1)
- behaviour-based system (1)
- binary countdown protocol (1)
- black bursts (1)
- classification (1)
- collaborative information visualization (1)
- collaborative mobile sensing (1)
- collective intelligence (1)
- computational biology (1)
- computational fluid dynamics (1)
- computer-supported cooperative work (1)
- concurrent (1)
- content-and-structure summary (1)
- continuous master theorem (1)
- crowd condition estimation (1)
- crowd density estimation (1)
- crowd scanning (1)
- crowd sensing (1)
- crowdsourcing (1)
- curves and surfaces (1)
- data sets (1)
- data-flow (1)
- dataset (1)
- decidability (1)
- design (1)
- deterministic arbitration (1)
- directed graphs (1)
- distributed (1)
- distributed real-time systems (1)
- distributed tasks (1)
- embedded (1)
- embedding (1)
- emotion visualization (1)
- end-to-end learning (1)
- environmental noise (1)
- evolutionary algorithm (1)
- firewall (1)
- flow visualization (1)
- foundational translation validation (1)
- gaussian filter (1)
- geographic information systems (1)
- geology (1)
- graph drawing algorithm (1)
- graph embedding (1)
- graph layout (1)
- historical documents (1)
- hypergraph (1)
- iB2C (1)
- image analysis (1)
- implementation (1)
- information systems (1)
- interference (1)
- interval arithmetic (1)
- invariant (1)
- language definition (1)
- language modeling (1)
- language profiles (1)
- linked data (1)
- long short-term memory (1)
- long tail (1)
- machine-checkable proof (1)
- magnetic field based localization (1)
- matrix visualization (1)
- message-passing (1)
- metadata (1)
- mixed-signal (1)
- modularisation (1)
- moment (1)
- multicore (1)
- multidimensional datasets (1)
- multinomial regression (1)
- multithreading (1)
- multitype code coupling (1)
- multiway partitioning (1)
- nestable tangibles (1)
- optimization correctness (1)
- oscillating magnetic fields (1)
- out-of-order (1)
- parallel (1)
- participatory sensing (1)
- path cost models (1)
- pattern recognition (1)
- pivot sampling (1)
- point cloud (1)
- proof generating optimizer (1)
- ray casting (1)
- ray tracing (1)
- real-time tasks (1)
- relaxed memory models (1)
- robustness (1)
- secondary structure prediction (1)
- semantic web (1)
- small-multiples node-link visualization (1)
- social media (1)
- software comprehension (1)
- software engineering task (1)
- spatial statistics (1)
- static software structure (1)
- stationary sensing (1)
- statistics (1)
- structural summary (1)
- subjective evaluation (1)
- symbolic simulation (1)
- synchronous (1)
- system architecture (1)
- tabletop (1)
- task sequence (1)
- tensor (1)
- tensorfield (1)
- terrain rendering (1)
- time-varying flow fields (1)
- touch surfaces (1)
- translation contract (1)
- urban planning (1)
- user-centered design (1)
- vector field visualization (1)
- vectorfield (1)
- virtual reality (1)
- visual structure (1)
- weighted finite-state transducers (1)
- wireless signal (1)
- zeitabhängige Strömungen (1)
- Ähnlichkeit (1)
- Übersetzung (1)

#### Faculty / Organisational entity

- Fachbereich Informatik (139) (remove)

Termination of Rewriting
(1994)

More and more, term rewriting systems are applied in computer science aswell as in mathematics. They are based on directed equations which may be used as non-deterministic functional programs. Termination is a key property for computing with termrewriting systems.In this thesis, we deal with different classes of so-called simplification orderings which areable to prove the termination of term rewriting systems. Above all, we focus on the problemof applying these termination methods to examples occurring in practice. We introduce aformalism that allows clear representations of orderings. The power of classical simplifica-tion orderings - namely recursive path orderings, path and decomposition orderings, Knuth-Bendix orderings and polynomial orderings - is improved. Further, we restrict these orderingssuch that they are compatible with underlying AC-theories by extending well-known methodsas well as by developing new techniques. For automatically generating all these orderings,heuristic-based algorithms are given. A comparison of these orderings with respect to theirpowers and their time complexities concludes the theoretical part of this thesis. Finally, notonly a detailed statistical evaluation of examples but also a brief introduction into the designof a software tool representing the integration of the specified approaches is given.

In dieser Dissertation wird das Konzept der Gröbnerbasen für endlich erzeugte Monoid-und Gruppenringe verallgemeinert. Dabei werden Reduktionsmethoden sowohl zurDarstellung der Monoid- beziehungsweise Gruppenelemente, als auch zur Beschreibungder Rechtsidealkongruenz in den entsprechenden Monoid- beziehungsweise Gruppenrin-gen benutzt. Da im allgemeinen Monoide und insbesondere Gruppen keine zulässigenOrdnungen mehr erlauben, treten bei der Definition einer geeigneten Reduktionsrela-tion wesentliche Probleme auf: Zum einen ist es schwierig, die Terminierung einer Re-duktionsrelation zu garantieren, zum anderen sind Reduktionsschritte nicht mehr mitMultiplikationen verträglich und daher beschreiben Reduktionen nicht mehr unbedingteine Rechtsidealkongruenz. In dieser Arbeit werden verschiedene Möglichkeiten Reduk-tionsrelationen zu definieren aufgezeigt und im Hinblick auf die beschriebenen Problemeuntersucht. Dabei wird das Konzept der Saturierung, d.h. eine Polynommenge so zu er-weitern, daß man die von ihr erzeugte Rechtsidealkongruenz durch Reduktion erfassenkann, benutzt, um Charakterisierungen von Gröbnerbasen bezüglich der verschiedenenReduktionen durch s-Polynome zu geben. Mithilfe dieser Konzepte ist es gelungenfür spezielle Klassen von Monoiden, wie z.B. endliche, kommutative oder freie, undverschiedene Klassen von Gruppen, wie z.B. endliche, freie, plain, kontext-freie odernilpotente, unter Ausnutzung struktureller Eigenschaften spezielle Reduktionsrelatio-nen zu definieren und terminierende Algorithmen zur Berechnung von Gröbnerbasenbezüglich dieser Reduktionsrelationen zu entwickeln.

Automated theorem proving is a search problem and, by its undecidability, a very difficult one. The challenge in the development of a practically successful prover is the mapping of the extensively developed theory into a program that runs efficiently on a computer. Starting from a level-based system model for automated theorem provers, in this work we present different techniques that are important for the development of powerful equational theorem provers. The contributions can be divided into three areas: Architecture. We present a novel prover architecture that is based on a set-based compression scheme. With moderate additional computational costs we achieve a substantial reduction of the memory requirements. Further wins are architectural clarity, the easy provision of proof objects, and a new way to parallelize a prover which shows respectable speed-ups in practice. The compact representation paves the way to new applications of automated equational provers in the area of verification systems. Algorithms. To improve the speed of a prover we need efficient solutions for the most time-consuming sub-tasks. We demonstrate improvements of several orders of magnitude for two of the most widely used term orderings, LPO and KBO. Other important contributions are a novel generic unsatisfiability test for ordering constraints and, based on that, a sufficient ground reducibility criterion with an excellent cost-benefit ratio. Redundancy avoidance. The notion of redundancy is of central importance to justify simplifying inferences which are used to prune the search space. In our experience with unfailing completion, the usual notion of redundancy is not strong enough. In the presence of associativity and commutativity, the provers often get stuck enumerating equations that are permutations of each other. By extending and refining the proof ordering, many more equations can be shown redundant. Furthermore, our refinement of the unfailing completion approach allows us to use redundant equations for simplification without the need to consider them for generating inferences. We describe the efficient implementation of several redundancy criteria and experimentally investigate their influence on the proof search. The combination of these techniques results in a considerable improvement of the practical performance of a prover, which we demonstrate with extensive experiments for the automated theorem prover Waldmeister. The progress achieved allows the prover to solve problems that were previously out of reach. This considerably enhances the potential of the prover and opens up the way for new applications.

The validity of formulas w.r.t. a specification over first-order logic with a semantics based on all models is semi-decidable. Therefore, we may implement a proof procedure which finds a proof for every valid formula fully automatically. But this semantics often lacks intuition: Some pathological models such as the trivial model may produce unexpected results w.r.t. validity. Instead, we may consider just a class of special models, for instance, the class of all data models. Proofs are then performed using induction. But, inductive validity is not semi-decidable -- even for first-order logic. This theoretical drawback manifests itself in practical limitations: There are theorems that cannot be proved by induction directly but only generalizations can be proved. For their definition, we may have to extend the specification. Therefore, we cannot expect to prove interesting theorems fully automatically. Instead, we have to support user-interaction in a suitable way. In this thesis, we aim at developing techniques that enhance automatic proof control of (inductive) theorem provers and that enable user-interaction in a suitable way. We integrate our new proof techniques into the inductive theorem prover QuodLibet and validate them with various case studies. Essentially, we introduce the following three proof techniques: -We integrate a decision procedure for linear arithmetic into QuodLibet in a close way by defining new inference rules that perform the elementary steps of the decision procedure. This allows us to implement well-known heuristics for automatic proof control. Furthermore, we are able to provide special purpose tactics that support the manual speculation of lemmas if a proof attempt gets stuck. The integration improves the ability of the theorem prover to prove theorems automatically as well as its efficiency. Our approach is competitive with other approaches regarding efficiency; it provides advantages regarding the speculation of lemmas. -The automatic proof control searches for a proof by applying inference rules. The search space is not only infinite, but grows dramatically with the depth of the search. In contrast to this, checking and analyzing performed proofs is very efficient. As the search space also has a high redundancy, it is reasonable to reuse subproofs found during proof search. We define new notions for the contribution of proof steps to a proof. These notions enable the derivation of pruned proofs and the identification of superfluous subformulas in theorems. A proof may be reused in two ways: upward propagation prunes a proof by eliminating superfluous proof steps; sideward reuse closes an open proof obligation by replaying an already found proof. -For interactive theorem provers, it is essential not only to prove automatically as many lemmas as possible but also to restrict proof search in such a way that the proof process stops within a reasonable amount of time. We introduce different markings in the goals to be proved and the lemmas to be applied to restrict proof search in a flexible way: With a forbidden marking, we can simulate well-known approaches for applying conditional lemmas. A mandatory marking provides a new heuristics which is inspired by local contribution of proof steps. With obligatory and generous markings, we can fine-tune the degree of efficiency and extent of proof search manually. With an elaborate case study, we show the benefits of the different techniques, in particular the synergetic effect of their combination.

The visualization of numerical fluid flow datasets is essential to the engineering processes that motivate their computational simulation. To address the need for visual representations that convey meaningful relations and enable a deep understanding of flow structures, the discipline of Flow Visualization has produced many methods and schemes that are tailored to a variety of visualization tasks. The ever increasing complexity of modern flow simulations, however, puts an enormous demand on these methods. The study of vortex breakdown, for example, which is a highly transient and inherently three-dimensional flow pattern with substantial impact wherever it appears, has driven current techniques to their limits. In this thesis, we propose several novel visualization methods that significantly advance the state of the art in the visualization of complex flow structures. First, we propose a novel scheme for the construction of stream surfaces from the trajectories of particles embedded in a flow. These surfaces are extremely useful since they naturally exploit coherence between neighboring trajectories and are highly illustrative in nature. We overcome the limitations of existing stream surface algorithms that yield poor results in complex flows, and show how the resulting surfaces can be used a building blocks for advanced flow visualization techniques. Moreover, we present a visualization method that is based on moving section planes that travel through a dataset and sample the flow. By considering the changes to the flow topology on the plane as it moves, we obtain a method of visualizing topological structures in three-dimensional flows that are not accessible by conventional topological methods. On the same algorithmic basis, we construct an algorithm for the tracking of critical points in such flows, thereby enabling the treatment of time-dependent datasets. Last, we address some problems with the recently introduced Lagrangian techniques. While conceptually elegant and generally applicable, they suffer from an enormous computational cost that we significantly use by developing an adaptive approximation algorithm. This allows the application of such methods on very large and complex numerical simulations. Throughout this thesis, we will be concerned with flow visualization aspect of general practical significance but we will particularly emphasize the remarkably challenging visualization of the vortex breakdown phenomenon.

Modelling languages are important in the process of software development. The suitability of a modelling language for a project depends on its applicability to the target domain. Here, domain-specific languages have an advantage over more general modelling languages. On the other hand, modelling languages like the Unified Modeling Language can be used in a wide range of domains, which supports the reuse of development knowledge between projects. This thesis treats the syntactical and semantical harmonisation of modelling languages and their combined use, and the handling of complexity of modelling languages by providing language subsets - called language profiles - with tailor-made formal semantics definitions, generated by a profile tool. We focus on the widely-used modelling languages SDL and UML, and formal semantics definitions specified using Abstract State Machines.

Feature Based Visualization
(2007)

In this thesis we apply powerful mathematical tools such as interval arithmetic for applications in computational geometry, visualization and computer graphics, leading to robust, general and efficient algorithms. We present a completely novel approach for computing the arrangement of arbitrary implicit planar curves and perform ray casting of arbitrary implicit functions by jointly achieving, for the first time, robustness, efficiency and flexibility. Indeed we are able to render even the most difficult implicits in real-time with guaranteed topology and at high resolution. We use subdivision and interval arithmetic as key-ingredients to guarantee robustness. The presented framework is also well-suited for applications to large and unstructured data sets due to the inherent adaptivity of the techniques that are used. We also approach the topic of tensors by collaborating with mechanical engineers on comparative tensor visualization and provide them with helpful visualization paradigms to interpret the data.

Nowadays, accounting, charging and billing users' network resource consumption are commonly used for the purpose of facilitating reasonable network usage, controlling congestion, allocating cost, gaining revenue, etc. In traditional IP traffic accounting systems, IP addresses are used to identify the corresponding consumers of the network resources. However, there are some situations in which IP addresses cannot be used to identify users uniquely, for example, in multi-user systems. In these cases, network resource consumption can only be ascribed to the owners of these hosts instead of corresponding real users who have consumed the network resources. Therefore, accurate accountability in these systems is practically impossible. This is a flaw of the traditional IP address based IP traffic accounting technique. This dissertation proposes a user based IP traffic accounting model which can facilitate collecting network resource usage information on the basis of users. With user based IP traffic accounting, IP traffic can be distinguished not only by IP addresses but also by users. In this dissertation, three different schemes, which can achieve the user based IP traffic accounting mechanism, are discussed in detail. The inband scheme utilizes the IP header to convey the user information of the corresponding IP packet. The Accounting Agent residing in the measured host intercepts IP packets passing through it. Then it identifies the users of these IP packets and inserts user information into the IP packets. With this mechanism, a meter located in a key position of the network can intercept the IP packets tagged with user information, extract not only statistic information, but also IP addresses and user information from the IP packets to generate accounting records with user information. The out-of-band scheme is a contrast scheme to the in-band scheme. It also uses an Accounting Agent to intercept IP packets and identify the users of IP traffic. However, the user information is transferred through a separated channel, which is different from the corresponding IP packets' transmission. The Multi-IP scheme provides a different solution for identifying users of IP traffic. It assigns each user in a measured host a unique IP address. Through that, an IP address can be used to identify a user uniquely without ambiguity. This way, traditional IP address based accounting techniques can be applied to achieve the goal of user based IP traffic accounting. In this dissertation, a user based IP traffic accounting prototype system developed according to the out-of-band scheme is also introduced. The application of user based IP traffic accounting model in the distributed computing environment is also discussed.

Embedded systems have become ubiquitous in everyday life, and especially in the automotive industry. New applications challenge their design by introducing a new class of problems that are based on a detailed analysis of the environmental situation. Situation analysis systems rely on models and algorithms of the domain of computational geometry. The basic model is usually an Euclidean plane, which contains polygons to represent the objects of the environment. Usual implementations of computational geometry algorithms cannot be directly used for safety-critical systems. First, a strict analysis of their correctness is indispensable and second, nonfunctional requirements with respect to the limited resources must be considered. This thesis proposes a layered approach to a polygon-processing system. On top of rational numbers, a geometry kernel is formalised at first. Subsequently, geometric primitives form a second layer of abstraction that is used for plane sweep and polygon algorithms. These layers do not only divide the whole system into manageable parts but make it possible to model problems and reason about them at the appropriate level of abstraction. This structure is used for the verification as well as the implementation of the developed polygon-processing library.

In urban planning, sophisticated simulation models are key tools to estimate future population growth for measuring the impact of planning decisions on urban developments and the environment. Simulated population projections usually result in large, macro-scale, multivariate geospatial data sets. Millions of records have to be processed, stored, and visualized to help planners explore and analyze complex population patterns. We introduce a database driven framework for visualizing geospatial multidimensional simulation data based on the output from UrbanSim, a software for the analysis and planning of urban developments. The designed framework is extendable and aims at integrating empirical-stochastic methods and urban simulation models with techniques developed for information visualization and cartography. First, we develop an empirical model for the estimation of residential building types based on demographic household characteristics. The predicted dwelling type information is important for the analysis of future material use, carbon footprint calculations, and for visualizing simultaneously the results of land usage, density, and other significant parameters in 3D space. Our model uses multinomial logistic regression to derive building types at different scales. The estimated regression coefficients are applied to UrbanSim output in order to predict residential building types. The simulation results and the estimated building types are managed in an object-relational geodatabase. From the database, density, building types, and significant demographic variables are visually encoded as scalable, georeferenced 3D geometries and displayed on top of aerial photographs in a Google Earth visual synthesis. The geodatabase can be accessed and the visualization parameters can be chosen through a web-based user interface. The geometries are encoded in KML, Google's markup language, as ready-to-visualize data sets. The goal is to enhance human cognition by displaying abstract representations of multidimensional data sets in a realistic context and thus to support decision making in planning processes.

Sound surrounds us all the time and in every place in our daily life, may it be pleasant music in a concert hall or disturbing noise emanating from a busy street in front of our home. The basic properties are the same for both kinds of sound, namely sound waves propagating from a source, but we perceive it in different ways depending on our current mood or if the sound is wanted or not. In this thesis both pleasant sound as well as disturbing noise is examined by means of simulating the sound and visualizing the results thereof. However, although the basic properties of music and traffic noise are the same, one is interested in different features. For example, in a concert hall, the reverberation time is an important quality measure, but if noise is considered only the resulting sound level, for example on ones balcony, is of interest. Such differences are reflected in different methods of simulation and required visualizations, therefore this thesis is divided into two parts. The first part about room acoustics deals with the simulation and novel visualizations for indoor sound and acoustic quality measures, such as definition (original "Deutlichkeit") and clarity index (original "Klarheitsmaß"). For the simulation two different methods, a geometric (phonon tracing) and a wave based (FEM) approach, are applied and compared. The visualization techniques give insight into the sound behaviour and the acoustic quality of a room from a global as well as a listener based viewpoint. Furthermore, an acoustic rendering equation is presented, which is used to render interference effects for different frequencies. Last but not least a novel visualization approach for low frequency sound is presented, which enables the topological analysis of pressure fields based on room eigenfrequencies. The second part about environmental noise is concerned with the simulation and visualization of outdoor sound with a focus on traffic noise. The simulation instruction prescribed by national regulations is discussed in detail, and an approach for the computation of noise volumes, as well as an extension to the simulation, allowing interactive noise calculation, are presented. Novel visualization and interaction techniques for the calculated noise data, incorporated in an interactive three dimensional environment, enabling the easy comprehension of noise problems, are presented. Furthermore additional information can be integrated into the framework to enhance the visualization of noise and the usability of the framework for different usages.

Today’s high-resolution digital images and videos require large amounts of storage space and transmission bandwidth. To cope with this, compression methods are necessary that reduce the required space while at the same time minimize visual artifacts. We propose a compression method based on a piecewise linear color interpolation induced by a triangulation of the image domain. We present methods to speed up significantly the optimization process for finding the triangulation. Furthermore, we extend the method to digital videos. Laser scanners to capture the surface of three-dimensional objects are widely used in industry nowadays, e.g., for reverse engineering or quality measurement. Hand-held scanning devices have the advantage that the laser device can be moved to any position, permitting a scan of complex objects. But operating a hand-held laser scanner is challenging. The operator has to keep track of the scanned regions in his mind, and has no feedback of the sample density unless he starts the surface reconstruction after finishing the scan. We present a system to support the operator by computing and rendering high-quality surface meshes of the captured data online, i.e., while he is still scanning, and in real time. Furthermore, it color-codes the rendered surface to reflect the surface quality. Thereby, instant feedback is provided, resulting in better scans in less time.

Computer-based simulation and visualization of acoustics of a virtual scene can aid during the design process of concert halls, lecture rooms, theaters, or living rooms. Because, not only the visual aspect of the room is important, but also its acoustics. In factory floors noise reduction is important since noise is hazardous to health. Despite the obvious dissimilarity between our aural and visual senses, many techniques required for the visualization of photo-realistic images and for the auralization of acoustic environments are quite similar. Both applications can be served by geometric methods such as particle- and ray tracing if we neglect a number of less important effects. By means of the simulation of room acoustics we want to predict the acoustic properties of a virtual model. For auralization, a pulse response filter needs to be assembled for each pair of source and listener positions. The convolution of this filter with an anechoic source signal provides the signal received at the listener position. Hence, the pulse response filter must contain all reverberations (echos) of a unit pulse, including their frequency decompositions due to absorption at different surface materials. For the room acoustic simulation a method named phonon tracing, since it is based on particles, is developed. The approach computes the energy or pressure decomposition for each particle (phonon) sent out from a sound source and uses this in a second pass (phonon collection) to construct the response filters for different listeners. This step can be performed in different precision levels. During the tracing step particle paths and additional information are stored in a so called phonon map. Using this map several sound visualization approaches were developed. From the visualization, the effect of different materials on the spectral energy / pressure distribution can be observed. The first few reflections already show whether certain frequency bands are rapidly absorbed. The absorbing materials can be identified and replaced in the virtual model, improving the overall acoustic quality of the simulated room. Furthermore an insight into the pressure / energy received at the listener position is possible. The phonon tracing algorithm as well as several sound visualization approaches are integrated into a common system utilizing Virtual Reality technologies in order to facilitate the immersion into the virtual scene. The system is a prototype developed within a project at the University of Kaiserslautern and is still a subject of further improvements. It consists of a stereoscopic back-projection system for visual rendering as well as professional audio equipment for auralization purposes.

Layout analysis--the division of page images into text blocks, lines, and determination of their reading order--is a major performance limiting step in large scale document digitization projects. This thesis addresses this problem in several ways: it presents new performance measures to identify important classes of layout errors, evaluates the performance of state-of-the-art layout analysis algorithms, presents a number of methods to reduce the error rate and catastrophic failures occurring during layout analysis, and develops a statistically motivated, trainable layout analysis system that addresses the needs of large-scale document analysis applications. An overview of the key contributions of this thesis is as follows. First, this thesis presents an efficient local adaptive thresholding algorithm that yields the same quality of binarization as that of state-of-the-art local binarization methods, but runs in time close to that of global thresholding methods, independent of the local window size. Tests on the UW-1 dataset demonstrate a 20-fold speedup compared to traditional local thresholding techniques. Then, this thesis presents a new perspective for document image cleanup. Instead of trying to explicitly detect and remove marginal noise, the approach focuses on locating the page frame, i.e. the actual page contents area. A geometric matching algorithm is presented to extract the page frame of a structured document. It is demonstrated that incorporating page frame detection step into document processing chain results in a reduction in OCR error rates from 4.3% to 1.7% (n=4,831,618 characters) on the UW-III dataset and layout-based retrieval error rates from 7.5% to 5.3% (n=815 documents) on the MARG dataset. The performance of six widely used page segmentation algorithms (x-y cut, smearing, whitespace analysis, constrained text-line finding, docstrum, and Voronoi) on the UW-III database is evaluated in this work using a state-of-the-art evaluation methodology. It is shown that current evaluation scores are insufficient for diagnosing specific errors in page segmentation and fail to identify some classes of serious segmentation errors altogether. Thus, a vectorial score is introduced that is sensitive to, and identifies, the most important classes of segmentation errors (over-, under-, and mis-segmentation) and what page components (lines, blocks, etc.) are affected. Unlike previous schemes, this evaluation method has a canonical representation of ground truth data and guarantees pixel-accurate evaluation results for arbitrary region shapes. Based on a detailed analysis of the errors made by different page segmentation algorithms, this thesis presents a novel combination of the line-based approach by Breuel with the area-based approach of Baird which solves the over-segmentation problem in area-based approaches. This new approach achieves a mean text-line extraction error rate of 4.4% (n=878 documents) on the UW-III dataset, which is the lowest among the analyzed algorithms. This thesis also describes a simple, fast, and accurate system for document image zone classification that results from a detailed comparative analysis of performance of widely used features in document analysis and content-based image retrieval. Using a novel combination of known algorithms, an error rate of 1.46% (n=13,811 zones) is achieved on the UW-III dataset in comparison to a state-of-the-art system that reports an error rate of 1.55% (n=24,177 zones) using more complicated techniques. In addition to layout analysis of Roman script documents, this work also presents the first high-performance layout analysis method for Urdu script. For that purpose a geometric text-line model for Urdu script is presented. It is shown that the method can accurately extract Urdu text-lines from documents of different layouts like prose books, poetry books, magazines, and newspapers. Finally, this thesis presents a novel algorithm for probabilistic layout analysis that specifically addresses the needs of large-scale digitization projects. The presented approach models known page layouts as a structural mixture model. A probabilistic matching algorithm is presented that gives multiple interpretations of input layout with associated probabilities. An algorithm based on A* search is presented for finding the most likely layout of a page, given its structural layout model. For training layout models, an EM-like algorithm is presented that is capable of learning the geometric variability of layout structures from data, without the need for a page segmentation ground-truth. Evaluation of the algorithm on documents from the MARG dataset shows an accuracy of above 95% for geometric layout analysis.

Knowledge discovery from large and complex collections of today’s scientific datasets is a challenging task. With the ability to measure and simulate more processes at increasingly finer spatial and temporal scales, the increasing number of data dimensions and data objects is presenting tremendous challenges for data analysis and effective data exploration methods and tools. Researchers are overwhelmed with data and standard tools are often insufficient to enable effective data analysis and knowledge discovery. The main objective of this thesis is to provide important new capabilities to accelerate scientific knowledge discovery form large, complex, and multivariate scientific data. The research covered in this thesis addresses these scientific challenges using a combination of scientific visualization, information visualization, automated data analysis, and other enabling technologies, such as efficient data management. The effectiveness of the proposed analysis methods is demonstrated via applications in two distinct scientific research fields, namely developmental biology and high-energy physics. Advances in microscopy, image analysis, and embryo registration enable for the first time measurement of gene expression at cellular resolution for entire organisms. Analysis of highdimensional spatial gene expression datasets is a challenging task. By integrating data clustering and visualization, analysis of complex, time-varying, spatial gene expression patterns and their formation becomes possible. The analysis framework MATLAB and the visualization have been integrated, making advanced analysis tools accessible to biologist and enabling bioinformatic researchers to directly integrate their analysis with the visualization. Laser wakefield particle accelerators (LWFAs) promise to be a new compact source of highenergy particles and radiation, with wide applications ranging from medicine to physics. To gain insight into the complex physical processes of particle acceleration, physicists model LWFAs computationally. The datasets produced by LWFA simulations are (i) extremely large, (ii) of varying spatial and temporal resolution, (iii) heterogeneous, and (iv) high-dimensional, making analysis and knowledge discovery from complex LWFA simulation data a challenging task. To address these challenges this thesis describes the integration of the visualization system VisIt and the state-of-the-art index/query system FastBit, enabling interactive visual exploration of extremely large three-dimensional particle datasets. Researchers are especially interested in beams of high-energy particles formed during the course of a simulation. This thesis describes novel methods for automatic detection and analysis of particle beams enabling a more accurate and efficient data analysis process. By integrating these automated analysis methods with visualization, this research enables more accurate, efficient, and effective analysis of LWFA simulation data than previously possible.

Adaptive Extraction and Representation of Geometric Structures from Unorganized 3D Point Sets
(2009)

The primary emphasis of this thesis concerns the extraction and representation of intrinsic properties of three-dimensional (3D) unorganized point clouds. The points establishing a point cloud as it mainly emerges from LiDaR (Light Detection and Ranging) scan devices or by reconstruction from two-dimensional (2D) image series represent discrete samples of real world objects. Depending on the type of scenery the data is generated from the resulting point cloud may exhibit a variety of different structures. Especially, in the case of environmental LiDaR scans the complexity of the corresponding point clouds is relatively high. Hence, finding new techniques allowing the efficient extraction and representation of the underlying structural entities becomes an important research issue of recent interest. This thesis introduces new methods regarding the extraction and visualization of structural features like surfaces and curves (e.g. ridge-lines, creases) from 3D (environmental) point clouds. One main part concerns the extraction of curve-like features from environmental point data sets. It provides a new method supporting a stable feature extraction by incorporating a probability-based point classification scheme that characterizes individual points regarding their affiliation to surface-, curve- and volume-like structures. Another part is concerned with the surface reconstruction from (environmental) point clouds exhibiting objects that are more or less complex. A new method providing multi-resolutional surface representations from regular point clouds is discussed. Following the applied principles of this approach a volumetric surface reconstruction method based on the proposed classification scheme is introduced. It allows the reconstruction of surfaces from highly unstructured and noisy point data sets. Furthermore, contributions in the field of reconstructing 3D point clouds from 2D image series are provided. In addition, a discussion concerning the most important properties of (environmental) point clouds with respect to feature extraction is presented.

This PhD thesis aims at finding a global robot navigation strategy for rugged off-road terrain which is robust against inaccurate self-localization, scalable to large environments, but also cost-efficient, e.g. able to generate navigation paths which optimize a cost measure closely related to terrain traversability. In order to meet this goal, aspects of both metrical and topological navigation techniques are combined. A primarily topological map is extended with the previously lacking capability of cost-efficient path planning and map extension. Further innovations include a multi-dimensional cost measure for topological edges, a method to learn these costs based on live feedback from the robot and a set of extrapolation methods to predict the traversability costs for untraversed edges. The thesis presents two sophisticated new image analysis techniques to optimize cost prediction based on the shape and appearance of surrounding terrain. Experimental results indicate that the proposed global navigation system is indeed able to perform cost-efficient, large scale path planning. At the same time, the need to maintain a fine-grained, global world model which would reduce the scalability of the approach is avoided.

Most software systems are described in high-level model or programming languages. Their runtime behavior, however, is determined by the compiled code. For uncritical software, it may be sufficient to test the runtime behavior of the code. For safety-critical software, there is an additional aggravating factor resulting from the fact that the code must satisfy the formal specification which reflects the safety policy of the software consumer and that the software producer is obliged to demonstrate that the code is correct with respect to the specification using formal verification techniques. In this scenario, it is of great importance that static analyses and formal methods can be applied on the source code level, because this level is more abstract and better suited for such techniques. However, the results of the analyses and the verification can only be carried over to the machine code level, if we can establish the correctness of the translation. Thus, compilation is a crucial step in the development of software systems and formally verified translation correctness is essential to close the formalization chain from high-level formal methods to the machine-code level. In this thesis, I propose an approach to certifying compilers which achieves the aim of closing the formalization chain from high-level formal methods to the machine-code level by applying techniques from mathematical logic and programming language semantics. I propose an approach called foundational translation validation (FTV) in which the software producer implements an FTV system comprising a compiler and a specification and verification framework (SVF) which is implemented in higher-order logic (HOL). The most important part of the SVF is an explicit translation contract which comprises the formalizations of the source and the target languages of the compiler and the formalization of a binary translation correctness predicate corrTrans(S,T) for source programs S and target programs T. The formalizations of the languages are realized as deep embeddings in HOL. This enables one to declare the whole program in a formalized language as a HOL constant. The predicate formally specifies when T is considered to be a correct translation of S. Its definition is explicitly based on the program semantics definitions provided by the translation contract. Subsequent to the translation, the compiler translates the source and the target programs into their syntactic representations as HOL constants, S and T, and generates a proof of corrTrans(S,T). We call a compiler which follows the FTV approach a proof generating compiler. Our approach borrows the idea of representing programs in correctness proofs as logic constants from the foundational proof-carrying code (FPCC) approach. Novel features that distinquish our approach from further approaches to certifying compilers, such as proof-carrying code (PCC) and translation validation (TV) are the following: Firstly, the presence of an explicit translation contract formalized in HOL: The approaches PCC and TV do not formalize a translation contract explicitly. Instead of this, they incorporate operational semantics and translation correctness criterion in translation validation tools on the programming language level. Secondly, representation of programs in correctness proofs as logic constants: The approaches PCC and the TV translate programs into their representations as semantic abstractions that serve as inputs for translation validation tools. Thirdly, certification of program transformation chains: Unlike the TV approach, which certifies single program transformations, the FTV approach achieves the aim of certifying whole chains of program transformations. This is possible due to the fact that the translation contract provides, for all programming languages involved in the program transformation chain, definitions of program semantics functions which map programs to mathematical objects that are elements of a set with an (at least) partial order "<=". Then, the proof makes use of the fact that the relation "<=" is transitive. In this thesis, the feasibility of the FTV approach is exemplified by the implementation of an FTV system. The system comprises a compiler front-end that certifies its optimization phase and an accompanying SVF that is implemented in the theorem prover Isabelle/HOL. The compiler front-end translates programs in a small C-like programming language, performs three optimizations: constant folding, dead assignment elimination, and loop invariant hoisting, and generates translation certificates in the form of Isabelle/HOL theories. The main focus of the thesis is on the description of the SVF and its translation verification techniques.

Modern digital imaging technologies, such as digital microscopy or micro-computed tomography, deliver such large amounts of 2D and 3D-image data that manual processing becomes infeasible. This leads to a need for robust, flexible and automatic image analysis tools in areas such as histology or materials science, where microstructures are being investigated (e.g. cells, fiber systems). General-purpose image processing methods can be used to analyze such microstructures. These methods usually rely on segmentation, i.e., a separation of areas of interest in digital images. As image segmentation algorithms rarely adapt well to changes in the imaging system or to different analysis problems, there is a demand for solutions that can easily be modified to analyze different microstructures, and that are more accurate than existing ones. To address these challenges, this thesis contributes a novel statistical model for objects in images and novel algorithms for the image-based analysis of microstructures. The first contribution is a novel statistical model for the locations of objects (e.g. tumor cells) in images. This model is fully trainable and can therefore be easily adapted to many different image analysis tasks, which is demonstrated by examples from histology and materials science. Using algorithms for fitting this statistical model to images results in a method for locating multiple objects in images that is more accurate and more robust to noise and background clutter than standard methods. On simulated data at high noise levels (peak signal-to-noise ratio below 10 dB), this method achieves detection rates up to 10% above those of a watershed-based alternative algorithm. While objects like tumor cells can be described well by their coordinates in the plane, the analysis of fiber systems in composite materials, for instance, requires a fully three dimensional treatment. Therefore, the second contribution of this thesis is a novel algorithm to determine the local fiber orientation in micro-tomographic reconstructions of fiber-reinforced polymers and other fibrous materials. Using simulated data, it will be demonstrated that the local orientations obtained from this novel method are more robust to noise and fiber overlap than those computed using an established alternative gradient-based algorithm, both in 2D and 3D. The property of robustness to noise of the proposed algorithm can be explained by the fact that a low-pass filter is used to detect local orientations. But even in the absence of noise, depending on fiber curvature and density, the average local 3D-orientation estimate can be about 9° more accurate compared to that alternative gradient-based method. Implementations of that novel orientation estimation method require repeated image filtering using anisotropic Gaussian convolution filters. These filter operations, which other authors have used for adaptive image smoothing, are computationally expensive when using standard implementations. Therefore, the third contribution of this thesis is a novel optimal non-orthogonal separation of the anisotropic Gaussian convolution kernel. This result generalizes a previous one reported elsewhere, and allows for efficient implementations of the corresponding convolution operation in any dimension. In 2D and 3D, these implementations achieve an average performance gain by factors of 3.8 and 3.5, respectively, compared to a fast Fourier transform-based implementation. The contributions made by this thesis represent improvements over state-of-the-art methods, especially in the 2D-analysis of cells in histological resections, and in the 2D and 3D-analysis of fibrous materials.