Filtern
Erscheinungsjahr
- 2002 (45) (entfernen)
Dokumenttyp
- Dissertation (30)
- Buch (Monographie) (7)
- Wissenschaftlicher Artikel (3)
- Konferenzveröffentlichung (1)
- Habilitation (1)
- Masterarbeit (1)
- Sonstiges (1)
- Bericht (1)
Sprache
- Deutsch (33)
- Englisch (10)
- Mehrsprachig (2)
Volltext vorhanden
- ja (45) (entfernen)
Schlagworte
- Deutschland (4)
- Entwicklungskooperation (2)
- Geschichte (2)
- Globalisierung (2)
- Literatur (2)
- Mobilität (2)
- OBDD (2)
- OBDDs (2)
- Ostafrika (2)
- Präimplantationsdiagnostik (2)
- culture (2)
- n.a. (2)
- Öffentlichkeit (2)
- 20. Jh. (1)
- 20th Century (1)
- Abwasserreinigung (1)
- Afrika (1)
- Alexandre Promio (1)
- Algorithmus (1)
- Alternativkino (1)
- Altersversorgung (1)
- Anorexia nervosa (1)
- Asymmetrie (1)
- Australian Literature (1)
- Australien <Nordost> (1)
- Autoaggression (1)
- Beteiligung (1)
- Betroffenheit (1)
- Bezahltes Dating (1)
- Bezugsperson (1)
- Bhagavad Gita (1)
- Bildnis (1)
- Bioakkumulation (1)
- Bioethik (1)
- Bioethik <Motiv> (1)
- Biomedizin (1)
- Blue Rider (1)
- Bodenschutz (1)
- Bulimarexie (1)
- Canadian Literature (1)
- Carrier-Proteine (1)
- Counter-Globalization (1)
- DDT (1)
- Dalit (1)
- Datenstruktur (1)
- Deregulierung (1)
- Deutsche Bahn AG (1)
- Dissemination (1)
- Distributed Systems (1)
- Drift (1)
- EEG (1)
- EKP (1)
- Ecotoxicology (1)
- Einstellung (1)
- Einzugsgebiet (1)
- Eisenbahn (1)
- Emotionales Verhalten (1)
- Englisch (1)
- Entwicklungsethnologie (1)
- Entwicklungspolitik (1)
- Entwicklungszusammenarbeit (1)
- Erbkrankheit (1)
- Erweiterung (1)
- Ethnosoziologie (1)
- Europäische Gemeinschaften / Kommission (1)
- Europäisches Zivilgesetzbuch (1)
- Farbensehen (1)
- Feldforschung (1)
- Fernerkundung (1)
- Fertilitätsstörung (1)
- Fettsucht (1)
- Filmwissenschaft (1)
- Fish (1)
- Formal Verification (1)
- Forschungsethik (1)
- Fotografie (1)
- Frauenbewegung (1)
- Frauenforschung (1)
- Fremdenverkehr (1)
- Gas Chromatography (1)
- Gegen-Globalisierung (1)
- Geistige Behinderung (1)
- Genklonierung (1)
- Geoinformationssystem (1)
- Geschichte 1800-1900 (1)
- Gesetzliche Krankenversicherung (1)
- Gesetzliche Krankenversicherung / Strukturreform (1)
- Gesundheitsreform (1)
- Gesundheitswesen (1)
- Gesundheitswesen / Reform (1)
- Gewässerschutz (1)
- Glokalisierung (1)
- Goethes Mater Gloriosa (1)
- Großbritannien (1)
- Harem (1)
- Hemisphaere (1)
- Hemisphäre <Anatomie> (1)
- Hemisphärendominanz (1)
- Hilfe (1)
- Hotelgewerbe (1)
- Hughes (1)
- Humangenetik (1)
- Hydrodynamik (1)
- Hyperlink-Management (1)
- Indian Philosophy (1)
- Informationseffizienz (1)
- Integrated Circuits (1)
- Integration (1)
- Interkulturalität (1)
- Japan (1)
- Kaiserpanorama (1)
- Kanada (1)
- Kanadische Literatur (1)
- Kerala (1)
- Keralite women (1)
- Klassische (1)
- Klonierung (1)
- Kommission für Europäisches Vertragsrecht (1)
- Kooperation (1)
- Kopfpauschalen (1)
- Korpus <Linguistik> (1)
- Korpuslinguistik (1)
- Krebskranker (1)
- Kreditmarkt (1)
- Kräuterbuch (1)
- Kultur (1)
- Kulturerbe (1)
- Kunst und Natur (1)
- Landwirtschaft (1)
- Lateralitaet (1)
- Lebensereignis (1)
- Linguistische Datenverarbeitung (1)
- Lobbyarbeit (1)
- Lobbyismus (1)
- Logischer Entwurf (1)
- Lumière (1)
- Malerei (1)
- Mangrove (1)
- Marias Gürtelspende (1)
- Marktsegmentierung (1)
- Maskerade <Motiv> (1)
- Maskerade von Charakter und Text (1)
- Masquerade of Characters and Text (1)
- Massenmedien (1)
- Medien (1)
- Medien / Wandel (1)
- Medienereignis (1)
- Mental Retardation (1)
- Metamorphosen (1)
- Methodismus (1)
- Middleware (1)
- Mitteleuropa (1)
- Mobile Networks (1)
- Mobile Telekommunikation (1)
- Modellrechnung (1)
- Motif of Disguise (1)
- Motivation (1)
- Multivariate Analyse (1)
- N-load (1)
- Naturkunst (1)
- Naturmaterial (1)
- Naturwandel (1)
- Naturwissenschaften (1)
- Oberflächenströmung (1)
- Ordered Binary Decision Diagrams (1)
- Osteuropa (1)
- Ovid (1)
- P300 (1)
- PRA (1)
- Participatory Appraisal (1)
- Partizipation (1)
- Pauschalprämien (1)
- Pflanzendarstellung (1)
- Philologie (1)
- Pietismus (1)
- Polychlorierte Biphenyle (1)
- Post-colonialism (1)
- Poststrukturalismus (1)
- Protektionismus (1)
- Psychobiologie (1)
- Raumordnung (1)
- Recht <Motiv> (1)
- Rechtsstellung des Embryos (1)
- Reform (1)
- Reise (1)
- Reproduction (1)
- Rheinland-Pfalz (1)
- Richard Hamann (1)
- Rukwa (1)
- Rürup-Kommission (1)
- Saarland (1)
- Salzgehalt (1)
- Samen (1)
- Schudra (1)
- Self-injurious Behavior (1)
- Sibirien (1)
- Southeast Asia (1)
- Soziale Unterstützung (1)
- Soziales Netzwerk (1)
- Sozialgesetzbuch 5 (1)
- Special Education (1)
- Sprachstatistik (1)
- Stammzellenforschung (1)
- Stammzellforschung (1)
- Stickstoffbelastung (1)
- Stressbewältigung (1)
- Synergetik (1)
- Systemtheorie (1)
- Ted (1)
- Terrorismus (1)
- Tizian (1)
- Transculturalism (1)
- Transitionssystem (1)
- Transkranielle magnetische Stimulation (1)
- Transkulturalismus (1)
- Translokalität (1)
- Transparenz (1)
- USA (1)
- Umweltbewusstsein (1)
- Vereinheitlichung (1)
- Vereinte Nationen / Charta (1)
- Verifikation (1)
- Verkehr (1)
- Verkehrsentwicklung (1)
- Verkehrsmittelwahl (1)
- Verkehrspolitik (1)
- Verkleidung <Motiv> (1)
- Verkleidungs-Motiv (1)
- Verteiltes System (1)
- Verteilung (1)
- Völkerkunde (1)
- Völkerrecht (1)
- Walheim (1)
- Wassergüte (1)
- Website-Management (1)
- Weltgesellschaft (1)
- Werefkin, Marianne von (1)
- Wurzelraum (1)
- XOR Parity (1)
- Xenobiotics (1)
- Zebrabärbling (1)
- Zwischenmenschliche Beziehung (1)
- abstraction (1)
- autonome regulation (1)
- burrows (1)
- capitation (1)
- cardiovascular reactivity (1)
- change of nature (1)
- code of ethics (1)
- color (1)
- contemporary art (1)
- coping behavior (1)
- corpus linguistics (1)
- cultural environment (1)
- deutsche Kräuterbücher des Mittelalters; mittelalterliches Naturverständnis (1)
- development anthropology (1)
- diversity (1)
- eating disorders (1)
- emotional reactions (1)
- empowerment-in-cinema (1)
- enjo kÅsai (1)
- equal distribution (1)
- explicit (1)
- flushing (1)
- formal verification (1)
- funerary monuments (1)
- genomic structure (1)
- geographic information systems (1)
- haelth care reform (1)
- headwater catchments (1)
- help seeking behavior (1)
- home pages (1)
- hotel (1)
- hydrodynamics (1)
- implicit (1)
- income distribution (1)
- indisches Kino (1)
- information retrieval (1)
- inn (1)
- integration (1)
- knights tombs (1)
- lifestyles (1)
- mangrove (1)
- medieval sepulcher art (1)
- memorial sculpture (1)
- memory (1)
- metabolism (1)
- metamorphoses (1)
- mobility decisions (1)
- morals (1)
- motives (1)
- mutation (1)
- nature and art (1)
- non-point pollution (1)
- obesity (1)
- partitioning (1)
- partizipative Methoden (1)
- precision farming (1)
- public sphere (1)
- quantitative Linguistik (1)
- quantitative linguistics (1)
- remote sensing (1)
- reordering (1)
- resource management (1)
- rumination (1)
- salt (1)
- search engine (1)
- self-interest (1)
- social support networks (1)
- soil and water conservation (1)
- spatial variability of water chemistry (1)
- spectralanalysis (1)
- spiritual groups (1)
- synergetics (1)
- systems theory (1)
- test (1)
- tourism (1)
- uncoupling protein (1)
- web-based services (1)
- zeitgenössische Kunst (1)
- Ägypten (1)
- Ästuar (1)
- Ökologie (1)
Institut
Untersuchung der Metamorphosen unter dem Gesichtspunkt der Veränderung auf der metatextuellen, diachronistischen und hypertextuellen Ebene in Ted Hughes' Tales from Ovid; übersetzungstheoretische wie textpragmatische und literaturphilosophische Überlegungen führen zum Schluss, dass die Veränderung der Form und des Stils des Epos die einzig signifikatstreue Form der Konservierung des Geists der Metamorphosen sein kann.
The painter Marianne Werefkin (born 1860; died 1938), from the circle of artists known as the Blue Rider (Der Blaue Reiter) in Munich and lifelong companion of Alexej Jawlenskys, lived in Russia and Latvia the first 36 years of her life. She received her artistic education in Moscow and St. Petersburg. Nevertheless the influence of Russian art on her Munich creative phase has been until now been omitted from research literature. Hence it lacks an important basis for the understanding of her creative output. In many respects Marianne Werefkin led the way in bringing the goals of so-called Russian Realism (russischen Realismus) onto another level, one in which the transmission of emotions was seen as a central aspect. The way the pictures of her teacher Ilja Repin had nothing to do with superficial emotion through simple moralistic categorization, but rather the painter demonstrated life's interconnectedness. After a new artistic beginning in Munich Werefkin took out the historical-daily context from her motifs, since, in the spirit of her time, she had recognized that everything visible was illusion. However she made use of actual reality as a repertoire of symbols for her own feelings, representing universal situations and allowing the total picture space to be the bearer of emotions. In that respect she is different from Wassily Kandinsky, who employed abstraction until reference to reality dissolved. Art for Werefkin involved no self-purpose, but should have a positive influence upon the observer. Narrative instruction is pushed to the background through the way it interacts, which depends upon knowledge of psychology and spiritual groups.
Insbesondere im wissenschaftlichen Bereich ist es zur Selbstverständlichkeit geworden, zur Befriedigung eines Informationsbedürfnisses zunächst das World Wide Web (Web) zu benutzen. Der komplexe Aufbau des Webs und die dort herrschende Unordnung machen das Auffinden bestimmter Dokumente zu einem diffizilen Vorgang. Suchmaschinen und Web-Verzeichnisse unterstützen den Benutzer hierbei; ihre effektive Nutzung ist jedoch nicht einfach. Es ist daher hilfreich, Suchdienste zu entwickeln, welche Kontextwissen mitbringen. In der vorliegenden Arbeit wird das Verfahren der thematisch spezialisierten Suche präsentiert und anhand der Menge der persönlicher Home Pages von Informatikern exemplifiziert. Der Bibliographie-Server DBLP.uni-trier.de liefert u.a. zu über 4.000 Wissenschaftlern manuell gesammelte persönliche Home Pages. Durch verschiedene Analysen werden in dieser Menge häufig vorkommende, also relevante Eigenschaften ermittelt. Dies ist ein kreativer Prozess, in den sowohl Suchwissen -- Wissen über Techniken des Suchens im Web -- als auch Fachwissen -- Wissen über die Beschaffenheit persönlicher Home Pages -- einfließen. Nach der Überprüfung dieser Eigenschaften auf ihre Signifikanz in der Gesamtheit der Web-Dokumente ist ein thematisch spezialisiertes Wissen erschaffen worden. Zur Durchführung der Suche würde man idealerweise alle Web-Dokumente mit Hilfe des erarbeiteten Wissens und des Anfrageterms -- des vollständigen Namens eines Informatikers -- untersuchen. Da das Web aus mehreren Milliarden Dokumenten besteht, ist dies praktisch nicht durchführbar: Es ist notwendig, eine geeignete Vorauswahl zu treffen. Suchmaschinen haben Daten zu vielen Web-Dokumenten erfasst. Deshalb wird mit ihrer Hilfe unter Verwendung des Anfrageterms eine Vorauswahl getroffen. Um nun die Dokumente der Vorauswahlmenge gemäß der Anfrage zu bewerten wird das thematisch spezialisierte Wissen adäquat in einer Bewertungsfunktion repräsentiert, welche jedem Dokument einen Wert zuweist und somit eine Rangfolge erstellt. Das Design der Bewertungsfunktion ist eine schöpferische Tätigkeit: Die sachgerechte Gewichtung der verschiedenen Eigenschaften bestimmt maßgeblich das Gelingen des Verfahrens. Der vornehmlich in Java implementierte, vollautomatisierte Web-Dienst HomePageSearch (hpsearch.uni-trier.de) führt regelmäßig für über 100.000 Namen diesen Suchvorgang durch. Der Benutzer kann auf das in einer DB2-Datenbank gespeicherte Ergebnis zurückgreifen. Durch die periodische Neuberechnung des thematisch spezialisierten Wissens wird der Dynamik des Webs Rechnung getragen. Der modulare und stark parametrisierte Aufbau des Systems erleichtert die Portierung des Verfahrens auf andere Mengen von Web-Dokumenten. Nicht zuletzt aufgrund der starken Verlinkung mit DBLP und ResearchIndex wird HomePageSearch von vielen Wissenschaftlern intensiv genutzt.
Hardware bugs can be extremely expensive, financially. Because microprocessors and integrated circuits have become omnipresent in our daily live and also because of their continously growing complexity, research is driven towards methods and tools that are supposed to provide higher reliability of hardware designs and their implementations. Over the last decade Ordered Binary Decision Diagrams (OBDDs) have been well proven to serve as a data structure for the representation of combinatorial or sequential circuits. Their conciseness and their efficient algorithmic properties are responsible for their huge success in formal verification. But, due to Shannon's counting argument, OBDDs can not always guarantee the concise representation of a given design. In this thesis, Parity Ordered Binary Decision Diagrams are presented, which are a true extension of OBDDs. In addition to the regular branching nodes of an OBDD, functional nodes representing a parity operation are integrated into the data structure, thus resulting in Parity-OBDDs. Parity-OBDDs are more powerful than OBDDs are, but, they are no longer a canonical representation. Besides theoretical aspects of Parity-OBDDs, algorithms for their efficient manipulation are the main focus of this thesis. Furthermore, an analysis on the factors that influence the Parity-OBDD representation size gives way for the development of heuristic algorithms for their minimization. The results of these analyses as well as the efficiency of the data structure are also supported by experiments. Finally, the algorithmic concept of Parity-OBDDs is extended to Mod-p-Decision Diagrams (Mod-p-DDs) for the representation of functions that are defined over an arbitrary finite domain.
Ausgehend davon, daß die nachweislich prominente Berichterstattung über bezahltes Dating sich nicht auf einen hohen Nachrichtenwert zurückführen läßt, sondern auf verkaufstechnische Faktoren und vor allem auf das "kulturelle Potential" des Themas Jugend, untersucht die folgende Arbeit, welche Normen und Werte in der Darstellung des Phänomens propagiert wurden, und ob sich in der Darstellung Muster erkennen lassen.
Von roten Autos und blauen Töpfen: Farbinformationen in impliziten und expliziten Gedächtnistests
(2002)
In fünf Experimenten wurden Erinnerungen an das Merkmal Farbe geprüft. Dabei wurden speziell implizite Gedächtnistests eingesetzt, in denen eine Bearbeitung ohne Verweis auf eine vorangegangene Lernphase und explizite Erinnerungsaufforderung erfolgte. Die empirischen Befunde in diesen Verfahren sprechen eindeutig gegen die in der Gedächtnispsychologie weit verbreiteten Kennzeichnung der Farbe als "irrelevante" Merkmalsdimension. So zeigte sich in der Farbwahlaufgabe der Einfluss der Farbe auf die Gedächtnisleistung, indem wiederholten schwarzweißen Testreizen die korrekte Zielfarbe häufiger spontan zugewiesen wurde als den neuen Stimuli. Dieser Wiederholungseffekt wurde weder durch den Formatwechsel von Bildern zu Wörtern, noch durch den Wechsel des abgebildeten Darstellungsexemplars beeinträchtigt, so dass von einer primär abstrakt-konzeptuellen Vermittlung auszugehen ist. Ein Farbeffekt war auch in zwei neu konstruierten impliziten Gedächtnistests zu verzeichnen. Zudem ergaben sich für die Aufgabe, in der die präferierte Farbe anzugeben war, erste Hinweise auf eine Beteiligung datengesteuerter Prozesse. Gängige Einschätzungen, nach denen die Farbe in solchen perzeptuellen impliziten Tests generell keine Rolle spielt, konnten damit erstmalig widerlegt werden. Zusätzlich erhobene explizite Testversionen erbrachten zum Teil erheblich abweichende Ergebnismuster. Offenbar wurde im impliziten Test von gespeicherten Informationen anders Gebrauch gemacht, als wenn das bewusste Erinnern der Studierepisode gefordert war.
Mobile computing poses different requirements on middleware than more traditional desktop systems interconnected by fixed networks. Not only the characteristics of mobile network technologies as for example lower bandwidth and unreliability demand for customized support. Moreover, the devices employed in mobile settings usually are less powerful than their desktop counterparts. Slow processors, a fairly limited amount of memory, and smaller displays are typical properties of mobile equipment, again requiring special treatment. Furthermore, user mobility results in additional requirements on appropriate middleware support. As opposed to the quite static environments dominating the world of desktop computing, dynamic aspects gain more importance. Suitable strategies and techniques for exploring the environment e.g. in order to discover services available locally are only one example. Managing resources in a fault-tolerant manner, reducing the impact ill-behaved clients have on system stability define yet another exemplary prerequisite. Most state of the art middleware has been designed for use in the realm of static, resource rich environments and hence is not immediately applicable in mobile settings as set forth above. The work described throughout this thesis aims at investigating the suitability of different middleware technologies with regard to application design, development, and deployment in the context of mobile networks. Mostly based upon prototypes, shortcomings of those technologies are identified and possible solutions are proposed and evaluated where appropriate. Besides tailoring middleware to specific communication and device characteristics, the cellular structure of current mobile networks may and shall be exploited in favor of more scalable and robust systems. Hence, an additional topic considered within this thesis is to point out and investigate suitable approaches permitting to benefit from such cellular infrastructures. In particular, a system architecture for the development of applications in the context of mobile networks will be proposed. An evaluation of this architecture employing mobile agents as flexible, network-side representatives for mobile terminals is performed, again based upon a prototype application. In summary, this thesis aims at providing several complementary approaches regarding middleware support tailored for mobile, cellular networks, a field considered to be of rising importance in a world where mobile communication and particularly data services emerge rapidly, augmenting the globally interconnecting, wired Internet.
This doctoral dissertation examines two authors of German descent who are representatives for the development of Canadian literature and its regional focus on the prairies: Frederick Philip Grove (1879-1948) and Robert Kroetsch (*1927). Kroetsch, in his essays and talks, has repeatedly referred to Grove as one of his "literary ancestors". Although there exist monographs and numerous articles on both authors, the present study is the first-ever comparative approach. This study's main access is provided by the motif of disguise and masquerade, which plays a central role in the authors' works. Even if critics have looked at the traditional motif (cf. Homer's Odyssey, or many Renaissance plays) in Kroetsch's writing sporadically, and have used it to examine Grove's biography, no approach has attempted a larger contextualization within/among both writers' oeuvres. According to Lloyd Davis, however, the motif can be seen as "representing the cultural dialogism, rather than any particular thesis, of selfhood" (Davis 16). Hence, it helps interrogate a topic that within Canada - the former colony and current multicultural immigrant society - had and has a specific relevance. As an analytical tool, the motif allows for highlighting both the similarities and the differences between the œuvres of Grove and Kroetsch as key-figures of a (post)colonial literature of Western Canada on the one hand, and for general questions pertaining to the characterisation of figures, the definition of narrative positions and even of genres on the other hand. Following the preface, two theoretical chapters outline conceptions of identity and their deducible forms and functions of disguise and masquerade, including a discussion of John Richardson's Wacousta (1832), which is the first Canadian example for the motif's constitutive use. The second major section sketches, in two separate chapters, the poetics and mentalities (Mentalitätsgeschichte) of each writer within the context of their complete works by looking at biographical data as well as the critics' assessments. After immigrating into Manitoba in 1912, Grove soon became the first representative of a literary prairie-realism. Before, he had faked his suicide in 1909 and stripped off his 'original' identity as the German translator (e.g., Wilde, Wells, Flaubert) as well as modestly successful poet and novelist Felix Paul Greve to leave behind debts and a notorious lover and to reinvent himself in the New World. The protean role-plays of 'FPG' - decoded only 23 years after his death - are manifested in his creation of literary characters, in a "collectivity of identities" (Cavell 12) or number of metonymic personae that keep his critics busy to this date. Providing a different story, Kroetsch's family of German background immigrated into Canada in the mid-19th-century. Kroetsch has been thematizing his native province, Alberta, just as much as general national dispositions or questings in the course of his literary career spanning five decades now. His progressive and experimental writing has earned him, for instance, the label of "Mr Canadian Postmodern" by Linda Hutcheon (Canadian Postmodern 183). Particularly important among his specifically postmodern instruments is the principle of archaeology as derived from Foucault and employed as both metaphor and method; further methodological tools are Barthes' theories on reading/writing as an erotic act, Bakhtin's notion of (the) carnival(ization of literature) and a great sensibility for the myths as well as oral traditions of the North American Natives. If the third section analyzes two of FPG's novels to illustrate his transfer, or literal translation, from a German to a Canadian cultural context, the fourth section represents this study's core with three one-to-one comparisons of the two writers' central prose texts. In spite of all affinities between both authors, however, this section already indicates what section five further underlines: Kroetsch clearly transcends Grove's achievements (which ultimately reduce all his characters and texts to nothing but his own will- and wishful projections and identity-configurations); on the level of narrativity, genre and gender, Kroetsch not only goes far beyond parodying Grove, but proves to be an innovator whose mis-en-scène of the motif of disguise provides both more psychological depth and relevance for socio-historical contexts. This comparative study has been informed by research in the Special Archives and Collections at the University of Manitoba (Grove Papers) and at the University of Calgary (Kroetsch Papers), by related talks at Lund, Belfast and Winnipeg as well as by an occasional quotation from an interview I conducted with Robert Kroetsch as early as 1996.
Today, usage of complex circuit designs in computers, in multimedia applications and communication devices is widespread and still increasing. At the same time, due to Moore's Law we do not expect to see an end in the growth of the complexity of digital circuits. The decreasing ability of common validation techniques -- like simulation -- to assure correctness of a circuit design enlarges the need for formal verification techniques. Formal verification delivers a mathematical proof that a given implementation of a design fulfills its specification. One of the basic and during the last years widely used data structure in formal verification are the so called Ordered Binary Decision Diagrams (OBDDs) introduced by R. Bryant in 1986. The topic of this thesis is integration of structural high-level information in the OBDD-based formal verification of sequential systems. This work consist of three major parts, covering different layers of formal verification applications: At the application layer, an assertion checking methodology, integrated in the verification flow of the high-level design and verification tool Protocol Compiler is presented. At the algorithmic layer, new approaches for partitioning of transition relations of complex finite state machines, that significantly improve the performance of OBDD-based sequential verification are introduced. Finally, at the data structure level, dynamic variable reordering techniques that drastically reduce the time required for reordering without a trade-off in OBDD-size are described. Overall, this work demonstrates how a tighter integration of applications by using structural information can significantly improve the efficiency of formal verification applications in an industrial setting.