Refine
Year of publication
Document Type
- Article (35791)
- Doctoral Thesis (6491)
- Monograph/Edited Volume (5553)
- Postprint (3296)
- Review (2292)
- Part of a Book (1065)
- Other (914)
- Preprint (567)
- Conference Proceeding (545)
- Part of Periodical (525)
Language
- English (30738)
- German (26053)
- Spanish (363)
- French (330)
- Italian (115)
- Russian (112)
- Multiple languages (68)
- Hebrew (36)
- Portuguese (25)
- Polish (24)
Keywords
- Germany (202)
- climate change (183)
- Deutschland (142)
- machine learning (83)
- European Union (79)
- diffusion (78)
- Sprachtherapie (77)
- morphology (74)
- Logopädie (73)
- Migration (73)
Institute
- Institut für Biochemie und Biologie (5459)
- Institut für Physik und Astronomie (5432)
- Institut für Geowissenschaften (3654)
- Institut für Chemie (3482)
- Wirtschaftswissenschaften (2645)
- Historisches Institut (2514)
- Department Psychologie (2348)
- Institut für Mathematik (2145)
- Institut für Romanistik (2108)
- Sozialwissenschaften (1883)
This thesis presents an attempt to use source code synthesised from Coq formalisations of device drivers for existing (micro)kernel operating systems, with a particular focus on the Linux Kernel.
In the first part, the technical background and related work are described. The focus is here on the possible approaches to synthesising certified software with Coq, namely the extraction to functional languages using the Coq extraction plugin and the extraction to Clight code using the CertiCoq plugin. It is noted that the implementation of CertiCoq is verified, whereas this is not the case for the Coq extraction plugin. Consequently, there is a correctness guarantee for the generated Clight code which does not hold for the code being generated by the Coq extraction plugin. Furthermore, the differences between user space and kernel space software are discussed in relation to Linux device drivers. It is elaborated that it is not possible to generate working Linux kernel module components using the Coq extraction plugin without significant modifications. In contrast, it is possible to produce working user space drivers both with the Coq extraction plugin and CertiCoq. The subsequent parts describe the main contributions of the thesis.
In the second part, it is demonstrated how to extend the Coq extraction plugin to synthesise foreign function calls between the functional language OCaml and the imperative language C. This approach has the potential to improve the type-safety of user space drivers. Furthermore, it is shown that the code being synthesised by CertiCoq cannot be used in kernel space without modifications to the necessary runtime. Consequently, the necessary modifications to the runtimes of CertiCoq and VeriFFI are introduced, resulting in the runtimes becoming compatible components of a Linux kernel module. Furthermore, justifications for the transformations are provided and possible further extensions to both plugins and solutions to failing garbage collection calls in kernel space are discussed.
The third part presents a proof of concept device driver for the Linux Kernel. To achieve this, the event handler of the original PC Speaker driver is partially formalised in Coq. Furthermore, some relevant formal properties of the formalised functionality are discussed. Subsequently, a kernel module is defined, utilising the modified variants of CertiCoq and VeriFFI to compile a working device driver. It is furthermore shown that it is possible to compile the synthesised code with CompCert, thereby extending the guarantee of correctness to the assembly layer. This is followed by a performance evaluation that compares a naive formalisation of the PC speaker functionality with the original PC Speaker driver pointing out the weaknesses in the formalisation and possible improvements. The part closes with a summary of the results, their implications and open questions being raised.
The last part lists all used sources, separated into scientific literature, documentations or reference manuals and artifacts, i.e. source code.
In weiten Teilen der Geschlechterforschung ist die Unterscheidung zwischen Privatheit und Öffentlichkeit von großer analytischer Bedeutung für das Verständnis moderner Geschlechterverhältnisse. Dennoch weisen ihre Analysen vielfach begriffliche Unschärfen im Gebrauch der Unterscheidung auf: Zum einen wird Familie mit Privatheit, Erwerbsarbeit mit Öffentlichkeit identisch gesetzt; zum anderen werden beide Unterscheidungen parallel verwendet. Der Beitrag setzt die beiden Unterscheidungen Privatheit/Öffentlichkeit und Familie/Erwerb mithilfe der Luhmann’schen Systemtheorie auf neue Weise ins Verhältnis. Dazu greift er den Forschungsansatz Doing Family auf, der Familie als Herstellungsleistung versteht. Vorgeschlagen wird, familiale Privatheit als staatlich geschützte familiale Selbststeuerungsebene zu begreifen, auf der sich die Familie gegenüber als öffentlich begriffenen Umwelterwartungen wie dem (dynamischen) Arbeitsmarkt sowohl abgrenzt als auch auf sie antwortet. Entsprechend besitzt jedes einzelne Familiensystem seine eigene Privatheit und Öffentlichkeit. Damit einhergehend, lassen sich die Individualisierung der Familienmitglieder als auch die zunehmende Irrelevanz von Gender für die familiale Binnenstruktur beobachten: Da jedes Familiensystem die Unterscheidung auf unterschiedliche Weise handhabt, findet eine Heterogenisierung von Familienformen statt.
This article examines how challenger parties enter the political arena and the effect of this entry by looking at the Italian 5 Star Movement (Movimento 5 Stelle – M5S). We explain the M5S's entry strategy in 2013 using the spatial approach to party competition and employing expert survey data collected for each national election between 2008 and 2018. These data allow us to analyse the changing spatial configuration of Italian politics due to the increasing salience of pro/anti-EU and pro/anti-immigration dimensions. We then apply the theoretical notion of the uncovered set (UCS) to trace how the M5S's entry reshaped the overall space of party competition, causing a realignment of existing parties. This work contributes to the ongoing debate on the electoral success of challenger parties and the emerging cleavages and polarization of party systems in Western European countries.
The bimolecular recombination characteristics of conjugated polymer poly[(4,4'-bis(2-ethylhexyl)dithieno[3,2-b:2',3'-d]silole)-2,6-diyl-alt-(2,5-bis 3-tetradecylthiophen-2-y1 thiazolo 5,4-d thiazole)-2,5diy1] (PDTSiTTz) blended with the fullerene series PC60BM, ICMA, ICBA, and ICTA have been investigated using microsecond and femtosecond transient absorption spectroscopy, in conjunction with electroluminescence measurements and ambient photoemission spectroscopy. The non-Langevin polymer PDTSiTTz allows an inspection of intrinsic bimolecular recombination rates uninhibited by diffusion, while the low oscillator strengths of fullerenes allow polymer features to dominate, and we compare our results to those of the well-known polymer Si-PCPDTBT. Using mu s-TAS, we have shown that the trap -limited decay dynamics of the PDTSiTTz polaron becomes progressively slower across the fullerene series, while those of Si-PCPDTBT are invariant. Electroluminescence measurements showed an unusual double peak in pristine PDTSiTTz, attributed to a low energy intragap charge transfer state, likely interchain in nature. Furthermore, while the pristine PDTSiTTz showed a broad, low-intensity density of states, the ICBA and ICTA blends presented a virtually identical DOS to Si-PCPDTBT and its blends. This has been attributed to a shift from a delocalized, interchain highest occupied molecular orbital (HOMO) in the pristine material to a dithienosilole-centered HOMO in the blends, likely a result of the bulky fullerenes increasing interchain separation. This HOMO localization had a side effect of progressively shifting the polymer HOMO to shallower energies, which was correlated with the observed decrease in bimolecular recombination rate and increased "trap" depth. However, since the density of tail states remained the same, this suggests that the traditional viewpoint of "trapping" being dominated by tail states may not encompass the full picture and that the breadth of the DOS may also have a strong influence on bimolecular recombination.
Understanding and constraining the source of geodetic deformation in volcanic areas is an important component of hazard assessment. Here, we analyse deformation and seismicity for one year before the March 2021 Fagradalsfjall eruption in Iceland. We generate a high-resolution catalogue of 39,500 earthquakes using optical cable recordings and develop a poroelastic model to describe three pre-eruptional uplift and subsidence cycles at the Svartsengi geothermal field, 8 km west of the eruption site. We find the observed deformation is best explained by cyclic intrusions into a permeable aquifer by a fluid injected at 4 km depth below the geothermal field, with a total volume of 0.11 ± 0.05 km3 and a density of 850 ± 350 kg m–3. We therefore suggest that ingression of magmatic CO2 can explain the geodetic, gravity and seismic data, although some contribution of magma cannot be excluded.
The Palaeocene-Eocene Thermal Maximum (ca. 56 million years ago) offers a primary analogue for future global warming and carbon cycle recovery. Yet, where and how massive carbon emissions were mitigated during this climate warming event remains largely unknown. Here we show that organic carbon burial in the vast epicontinental seaways that extended over Eurasia provided a major carbon sink during the Palaeocene-Eocene Thermal Maximum. We coupled new and existing stratigraphic analyses to a detailed paleogeographic framework and using spatiotemporal interpolation calculated ca. 720–1300 Gt organic carbon excess burial, focused in the eastern parts of the Eurasian epicontinental seaways. A much larger amount (2160–3900 Gt C, and when accounting for the increase in inundated shelf area 7400–10300 Gt C) could have been sequestered in similar environments globally. With the disappearance of most epicontinental seas since the Oligocene-Miocene, an effective negative carbon cycle feedback also disappeared making the modern carbon cycle critically dependent on the slower silicate weathering feedback.
This thesis focuses on the molecular evolution of Macroscelidea, commonly referred to as sengis. Sengis are a mammalian order belonging to the Afrotherians, one of the four major clades of placental mammals. Sengis currently consist of twenty extant species, all of which are endemic to the African continent. They can be separated in two families, the soft-furred sengis (Macroscelididae) and the giant sengis (Rhynchocyonidae). While giant sengis can be exclusively found in forest habitats, the different soft-furred sengi species dwell in a broad range of habitats, from tropical rain-forests to rocky deserts.
Our knowledge on the evolutionary history of sengis is largely incomplete. The high level of superficial morphological resemblance among different sengi species (especially the soft-furred sengis) has for example led to misinterpretations of phylogenetic relationships, based on morphological characters. With the rise of DNA based taxonomic inferences, multiple new genera were defined and new species described. Yet, no full taxon molecular phylogeny exists, hampering the answering of basic taxonomic questions. This lack of knowledge can be to some extent attributed to the limited availability of fresh-tissue samples for DNA extraction. The broad African distribution, partly in political unstable regions and low population densities complicate contemporary sampling approaches. Furthermore, the DNA information available usually covers only short stretches of the mitochondrial genome and thus a single genetic locus with limited informational content.
Developments in DNA extraction and library protocols nowadays offer the opportunity to access DNA from museum specimens, collected over the past centuries and stored in natural history museums throughout the world. Thus, the difficulties in fresh-sample acquisition for molecular biological studies can be overcome by the application of museomics, the research field which emerged from those laboratory developments.
This thesis uses fresh-tissue samples as well as a vast collection museum specimens to investigate multiple aspects about the macroscelidean evolutionary history. Chapter 4 of this thesis focuses on the phylogenetic relationships of all currently known sengi species. By accessing DNA information from museum specimens in combination of fresh tissue samples and publicly available genetic resources it produces the first full taxon molecular phylogeny of sengis. It confirms the monophyly of the genus Elephantulus and discovers multiple deeply divergent lineages within different species, highlighting the need for species specific approaches. The study furthermore focuses on the evolutionary time frame of sengis by evaluating the impact of commonly varied parameters on tree dating. The results of the study show, that the mitochondrial information used in previous studies to temporal calibrate the Macroscelidean phylogeny led to an overestimation of node ages within sengis. Especially soft-furred sengis are thus much younger than previously assumed. The refined knowledge of nodes ages within sengis offer the opportunity to link e.g. speciation events to environmental changes.
Chapter 5 focuses on the genus Petrodromus with its single representative Petrodromus tetradactylus. It again exploits the opportunities of museomics and gathers a comprehensive, multi-locus genetic dataset of P. tetradactylus individuals, distributed across most the known range of this species. It reveals multiple deeply divergent lineages within Petrodromus, whereby some could possibly be associated to previously described sub-species, at least one was formerly unknown. It underscores the necessity for a revision of the genus Petrodromus through the integration of both molecular and morphological evidence. The study, furthermore identifies changing forest distributions through climatic oscillations as main factor shaping the genetic structure of Petrodromus.
Chapter 6 uses fresh tissue samples to extent the genomic resources of sengis by thirteen new nuclear genomes, of which two were de-novo assembled. An extensive dataset of more than 8000 protein coding one-to-one orthologs allows to further refine and confirm the temporal time frame of sengi evolution found in Chapter 4. This study moreover investigates the role of gene-flow and incomplete lineage sorting (ILS) in sengi evolution. In addition it identifies clade specific genes of possible outstanding evolutionary importance and links them to potential phenotypic traits affected. A closer investigation of olfactory receptor proteins reveals clade specific differences. A comparison of the demographic past of sengis to other small African mammals does not reveal a sengi specific pattern.