Refine
Year of publication
Document Type
- Doctoral Thesis (6497) (remove)
Language
Keywords
- climate change (56)
- Klimawandel (55)
- Modellierung (36)
- Nanopartikel (28)
- machine learning (23)
- Fernerkundung (20)
- Spracherwerb (19)
- Synchronisation (19)
- Deutschland (18)
- remote sensing (18)
Institute
- Institut für Biochemie und Biologie (1042)
- Institut für Physik und Astronomie (782)
- Institut für Chemie (678)
- Institut für Geowissenschaften (506)
- Wirtschaftswissenschaften (407)
- Institut für Ernährungswissenschaft (278)
- Öffentliches Recht (252)
- Bürgerliches Recht (220)
- Historisches Institut (214)
- Institut für Informatik und Computational Science (206)
- Institut für Umweltwissenschaften und Geographie (202)
- Sozialwissenschaften (176)
- Extern (168)
- Department Psychologie (158)
- Institut für Mathematik (151)
- Department Linguistik (138)
- Department Sport- und Gesundheitswissenschaften (117)
- Department Erziehungswissenschaft (110)
- Hasso-Plattner-Institut für Digital Engineering GmbH (98)
- Institut für Romanistik (94)
- Institut für Germanistik (88)
- Strafrecht (80)
- Philosophische Fakultät (67)
- Institut für Jüdische Studien und Religionswissenschaft (57)
- Hasso-Plattner-Institut für Digital Engineering gGmbH (46)
- Institut für Anglistik und Amerikanistik (46)
- Institut für Künste und Medien (46)
- Institut für Philosophie (37)
- Department Musik und Kunst (26)
- Fachgruppe Betriebswirtschaftslehre (26)
- Fachgruppe Politik- & Verwaltungswissenschaft (26)
- Institut für Slavistik (25)
- Department Grundschulpädagogik (15)
- Strukturbereich Kognitionswissenschaften (15)
- Strukturbereich Bildungswissenschaften (11)
- Digital Engineering Fakultät (7)
- Fachgruppe Volkswirtschaftslehre (7)
- Potsdam Institute for Climate Impact Research (PIK) e. V. (7)
- MenschenRechtsZentrum (6)
- Department für Inklusionspädagogik (5)
- Fachgruppe Soziologie (5)
- Mathematisch-Naturwissenschaftliche Fakultät (5)
- Institut für Religionswissenschaft (4)
- Klassische Philologie (4)
- Lehreinheit für Wirtschafts-Arbeit-Technik (4)
- Psycholinguistics and Neurolinguistics (4)
- Kommunalwissenschaftliches Institut (3)
- Fakultät für Gesundheitswissenschaften (2)
- Institut für Jüdische Theologie (2)
- Interdisziplinäres Zentrum für Kognitive Studien (2)
- Juristische Fakultät (2)
- Multilingualism (2)
- Patholinguistics/Neurocognition of Language (2)
- Applied Computational Linguistics (1)
- Foundations of Computational Linguistics (1)
- Interdisziplinäres Zentrum für Dynamik komplexer Systeme (1)
- Language Acquisition (1)
- Phonology & Phonetics (1)
- Potsdam Research Institute for Multilingualism (PRIM) (1)
- Potsdam Transfer - Zentrum für Gründung, Innovation, Wissens- und Technologietransfer (1)
- Syntax, Morphology & Variability (1)
- Wirtschafts- und Sozialwissenschaftliche Fakultät (1)
Der Semi-Parlamentarismus beschreibt das Regierungssystem, in dem die Regierung von einem Teil des Parlaments gewählt wird und abberufen werden kann, von einem anderen Teil des Parlaments aber unabhängig ist. Beide Kammern müssen dabei der Gesetzgebung zustimmen. Dieses von Steffen Ganghof klassifizierte System ergänzt gängige Regierungssystemtypologien, wie sie beispielsweise von David Samuels und Matthew Shugart genutzt werden. Der Semi-Parlamentarismus ist der logische Gegenpart zum Semi-Präsidentialismus, bei dem nur ein Teil der Exekutive von der Legislative abhängt, während im Semi-Parlamentarismus die Exekutive von nur einem Teil der Legislative abhängt. Der Semi-Parlamentarismus verkörpert so ein System der Gewaltenteilung ohne einen exekutiven Personalismus, wie er durch die Direktwahl und Unabhängigkeit der Regierungchef:in im Präsidentialismus hervorgerufen wird. Dadurch ist der Semi-Parlamentarismus geeignet, Unterschiede zwischen Parlamentarismus und Präsidentialismus auf den separaten Einfluss der Gewaltenteilung und des exekutiven Personalismus zurückzuführen. Die Untersuchung des Semi-Parlamentarismus ist daher für die Regierungssystemliteratur insgesamt von Bedeutung. Der Semi-Parlamentarismus ist dabei kein rein theoretisches Konstrukt, sondern existiert im australischen Bundesstaat, den australischen Substaaten und Japan.
Die vorliegende Dissertation untersucht erstmals umfassend die Gesetzgebung der semi-parlamentarischen Staaten als solchen. Der Fokus liegt dabei auf den zweiten Kammern, da diese durch die Unabhängigkeit von der Regierung der eigentliche Ort der Gesetzgebung sind. Die Gesetzgebung in Parlamentarismus und Präsidentialismus unterscheidet sich insbesondere in der Geschlossenheit der Parteien, der Koalitionsbildung und dem legislativen Erfolg der Regierungen. Diese Punkte sind daher auch von besonderem Interesse bei der Analyse des Semi-Parlamentarismus. Die semi-parlamentarischen Staaten unterscheiden sich auch untereinander teilweise erheblich in der institutionellen Ausgestaltung wie den Wahlsystemen oder den verfügbaren Mitteln zur Überwindung von Blockadesituationen. Die Darstellung und die Analyse der Auswirkungen dieser Unterschiede auf die Gesetzgebung ist neben dem Vergleich des Semi-Parlamentarismus mit anderen Systemen das zweite wesentliche Ziel dieser Arbeit.
Als Fundament der Analyse habe ich einen umfangreichen Datensatz erhoben, der alle Legislaturperioden der australischen Staaten zwischen 1997 und 2019 umfasst. Wesentliche Bestandteile des Datensatzes sind alle namentlichen Abstimmungen beider Kammern, alle
eingebrachten und verabschiedeten Gesetzen der Regierung sowie die mit Hilfe eines Expert-Surveys erhobenen Parteipositionen in den relevanten Politikfeldern auf substaatlicher Ebene.
Hauptsächlich mit der Hilfe von Mixed-Effects- und Fractional-Response-Analysen kann ich so zeigen, dass der Semi-Parlamentarismus in vielen Aspekten eher parlamentarischen als präsidentiellen Systemen gleicht. Nur die Koalitionsbildung erfolgt deutlich flexibler und unterscheidet sich daher von der typischen parlamentarischen Koalitionsbildung. Die Analysen legen nahe, dass wesentliche Unterschiede zwischen Parlamentarismus und Präsidentialismus eher auf den exekutiven Personalismus als auf die Gewaltenteilung zurückzuführen sind.
Zwischen den semi-parlamentarischen Staaten scheinen vor allem die Kontrolle des Medians beider Parlamentskammern durch die Regierung und die Möglichkeit der Regierung, die zweite Kammer mitaufzulösen, zu entscheidenden Unterschieden in der Gesetzgebung zu führen. Die Kontrolle des Medians ermöglicht eine flexible Koalitionsbildung und führt zu höheren legislativen Erfolgsraten. Ebenso führt eine möglichst leichte Auflösungsmöglichkeit der zweiten Kammern zu höheren legislativen Erfolgsraten. Die Parteigeschlossenheit ist unabhängig von diesen Aspekten in beiden Kammern der semi-parlamentarischen Parlamente sehr hoch.
Digitale Medien erlangen eine zunehmende Bedeutung für die Gestaltung von unterrichtlichen Lehr- und Lernprozessen (KMK, 2021; Scheiter, 2021). Die erfolgreiche Integration digitaler Medien und die qualitätsvolle Gestaltung digitalgestützten Unterrichts ist dabei abhängig von den digitalen Kompetenzen der beteiligten Lehrkräfte (KMK, 2021; Lachner et al., 2020). Lehrkräftefortbildungen zu Themen digitaler Medien sind in diesem Kontext von großer Relevanz. Die Teilnahme an Fortbildungen zu digitalen Themen kann zur Förderung der (selbsteingeschätzten) digitalen Kompetenzen sowie des digitalgestützten Unterrichts beitragen (KMK, 2021; SWK, 2022). Die Zusammenhänge zwischen Lehrkräftefortbildungen, Kompetenzen und Handeln von Lehrkräften werden auf theoretischer Ebene im Modell der Determinanten und Konsequenzen der professionellen Kompetenz von Lehrkräften nach Kunter et al. (2011) beschrieben. Allerdings ist bislang ungeklärt, inwiefern die für allgemeine Lehrkräftefortbildungen formulierten Zusammenhänge auch auf den digitalen Kontext übertragbar sind. Bisher weisen nur wenige empirische Ergebnisse darauf hin, dass digitalbezogene Lehrkräftefortbildungen mit selbsteingeschätzten digitalen Kompetenzen (z. B. Mayer et al., 2021; Ning et al., 2022; Reisoğlu, 2022) und dem digitalgestützten Unterrichtshandeln zusammenhängen (z. B. Alt, 2018; Gisbert Cervera & Lázaro Cantabrana, 2015). Eine zentrale Rolle für qualitätsvolles Unterrichtshandeln spielen die Handlungskompetenzen von Lehrkräften (Kunter et al., 2011). Auch im digitalen Kontext sind (selbsteingeschätzte) Kompetenzen von Lehrkräften für das unterrichtliche Handeln mit digitalen Medien relevant (z. B. Hatlevik, 2017; Spiteri & Rundgren, 2020). Eine systematische Darstellung von Kompetenzen von Lehrkräften für den unterrichtsbezogenen Einsatz digitaler Medien leistet der European Framework for the Digital Competence of Educators (DigCompEdu; Redecker & Punie, 2017). Jedoch liegen bisher nur wenige empirische Forschungsarbeiten zur Validierung dieses Rahmenmodells vor (z. B. Antonietti et al., 2022). Dabei bietet das DigCompEdu-Modell im Vergleich zu anderen Kompetenzmodellen wie beispielsweise dem Modell des Technological Pedagogical Content Knowledge (TPACK; Mishra & Koehler, 2006) einen differenzierten Blick auf verschiedene Kompetenzdimensionen.
Die aufgezeigten Forschungslücken aufnehmend, befasst sich die vorliegende Dissertation mit den Faktoren, die zu einer hohen Unterrichtsqualität im digitalgestützten Unterricht beitragen. Die drei empirischen Studien dieser Dissertation behandeln aus verschiedenen Perspektiven die Zusammenhänge zwischen der Teilnahme an digitalbezogenen Lehrkräftefortbildungen, den selbsteingeschätzten digitalen Kompetenzen von Lehrkräften und der selbstberichteten digitalgestützten Unterrichtsqualität. Die Studien orientieren sich dabei theoriegeleitet an den Annahmen des Modells der Determinanten und Konsequenzen der professionellen Kompetenz von Lehrkräften nach Kunter et al. (2011).
Studie 1 widmet sich der Frage, inwieweit die Teilnahme an digitalbezogenen Fortbildungen und Lehrkräftekooperationen im digitalen Kontext mit selbsteingeschätzten digitalen Kompetenzen, Interesse am digitalgestützten Unterrichten und qualitätsvollem Unterrichten mit digitalen Medien zusammenhängen. Die Ergebnisse manifester Pfadmodelle verdeutlichen, dass die Teilnahme an digitalbezogenen Fortbildungen und Kooperationen mit hohen digitalen Kompetenzen, einem hohen Interesse am digitalgestützten Unterrichten und einem selbstberichteten häufigen Einsatz digitaler Medien zur Umsetzung qualitätsvollen Unterrichtens (kognitive Aktivierung und Individualisierung) einhergingen. Digitalgestütztes Unterrichtshandeln wurde in bisherigen empirischen Studien vorrangig über die Nutzungshäufigkeit digitaler Medien im Unterricht erhoben, welche jedoch keine Rückschlüsse auf die Qualität des Einsatzes zulässt (Lachner et al., 2020; Scheiter, 2021). Der qualitätsvolle Einsatz digitaler Medien entlang der drei generischen Basisdimensionen (Klieme et al., 2009) wird daher in allen drei Studien der Dissertation berücksichtigt. In Studie 1 konnte zudem gezeigt werden, dass die selbsteingeschätzten digitalen Kompetenzen im Bereich TPACK die querschnittlichen Zusammenhänge zwischen der Teilnahmehäufigkeit von Lehrkräften an digitalbezogenen Fortbildungen und der Nutzungshäufigkeit digitaler Medien zur Umsetzung von kognitiver Aktivierung und Individualisierung vermitteln.
In Studie 2 wurden Skalen zur Erfassung selbsteingeschätzter digitaler Kompetenzen basierend auf dem DigCompEdu-Modell entwickelt und getestet. Konkret wurde dabei die Kompetenzdimension der Lernerorientierung mit den Subdimensionen Differenzierung und Aktive Einbindung von Schüler*innen in den Blick genommen. Die Ergebnisse der durchgeführten Strukturgleichungsmodellierungen legen eine bifaktorielle Faktorstruktur nahe, die sowohl die zwei theoretisch angenommenen Subdimensionen repräsentiert als auch einen generellen Faktor beinhaltet, der sich als übergreifende Lernerorientierung interpretiert lässt. Die selbsteingeschätzten digitalen Kompetenzen in Bereich der Lernerorientierung standen in signifikant positivem Zusammenhang mit dem selbstberichteten Einsatz digitaler Medien zur selbstberichteten Umsetzung qualitätsvollen Unterrichtshandelns (Klassenführung, kognitive Aktivierung und konstruktive Unterstützung).
Studie 3 führt die Themenfelder der Fortbildungen und der Kompetenzen im digitalen Kontext zusammen und befasst sich mit dem Zusammenhang zwischen Fortbildungsthemen und digitalen Kompetenzen. Ergebnisse von Pfadmodellierungen zeigen, dass die Teilnahme an digitalbezogenen Fortbildungen zu den technologisch-pädagogisch-inhaltlichen Themen „Computergestützte Förderung der Schüler*innen“ und „Fachspezifische Unterrichtsentwicklung mit digitalen Medien“ mit dem selbstberichteten qualitätsvollen Einsatz digitaler Medien zur kognitiven Aktivierung und konstruktiven Unterstützung einhergehen. Diese Befunde stärken die Annahme, dass Lehrkräfte für einen qualitätsvollen Einsatz digitaler Medien sowohl technologische als auch pädagogisch didaktische Kompetenzen benötigen (Lipowsky & Rzejak, 2021; Mishra & Koehler, 2006; Scheiter & Lachner, 2019) und Fortbildungen folglich technologische mit unterrichtspraktischen Inhalten kombinieren sollten (Bonnes et al., 2022). Zudem zeigt die Studie basierend auf den theoretischen Annahmen von Kunter et al. (2011), dass selbsteingeschätzte digitale Kompetenzen von Lehrkräften die Zusammenhänge zwischen der Teilnahmehäufigkeit an digitalbezogenen Fortbildungen und der selbstberichteten digitalgestützten Unterrichtsqualität vermittelten.
In der abschließenden Gesamtdiskussion der Dissertation werden die Befunde vor dem Hintergrund des dargelegten Forschungsstandes und hinsichtlich der Forschungslücken diskutiert und auf Grundlage der Befunde der drei Studien forschungs- und praxisrelevante Implikationen abgeleitet.
Deep learning has seen widespread application in many domains, mainly for its ability to learn data representations from raw input data. Nevertheless, its success has so far been coupled with the availability of large annotated (labelled) datasets. This is a requirement that is difficult to fulfil in several domains, such as in medical imaging. Annotation costs form a barrier in extending deep learning to clinically-relevant use cases. The labels associated with medical images are scarce, since the generation of expert annotations of multimodal patient data at scale is non-trivial, expensive, and time-consuming. This substantiates the need for algorithms that learn from the increasing amounts of unlabeled data. Self-supervised representation learning algorithms offer a pertinent solution, as they allow solving real-world (downstream) deep learning tasks with fewer annotations. Self-supervised approaches leverage unlabeled samples to acquire generic features about different concepts, enabling annotation-efficient downstream task solving subsequently.
Nevertheless, medical images present multiple unique and inherent challenges for existing self-supervised learning approaches, which we seek to address in this thesis: (i) medical images are multimodal, and their multiple modalities are heterogeneous in nature and imbalanced in quantities, e.g. MRI and CT; (ii) medical scans are multi-dimensional, often in 3D instead of 2D; (iii) disease patterns in medical scans are numerous and their incidence exhibits a long-tail distribution, so it is oftentimes essential to fuse knowledge from different data modalities, e.g. genomics or clinical data, to capture disease traits more comprehensively; (iv) Medical scans usually exhibit more uniform color density distributions, e.g. in dental X-Rays, than natural images. Our proposed self-supervised methods meet these challenges, besides significantly reducing the amounts of required annotations.
We evaluate our self-supervised methods on a wide array of medical imaging applications and tasks. Our experimental results demonstrate the obtained gains in both annotation-efficiency and performance; our proposed methods outperform many approaches from related literature. Additionally, in case of fusion with genetic modalities, our methods also allow for cross-modal interpretability. In this thesis, not only we show that self-supervised learning is capable of mitigating manual annotation costs, but also our proposed solutions demonstrate how to better utilize it in the medical imaging domain. Progress in self-supervised learning has the potential to extend deep learning algorithms application to clinical scenarios.
Arctic climate change is marked by intensified warming compared to global trends and a significant reduction in Arctic sea ice which can intricately influence mid-latitude atmospheric circulation through tropo- and stratospheric pathways. Achieving accurate simulations of current and future climate demands a realistic representation of Arctic climate processes in numerical climate models, which remains challenging.
Model deficiencies in replicating observed Arctic climate processes often arise due to inadequacies in representing turbulent boundary layer interactions that determine the interactions between the atmosphere, sea ice, and ocean. Many current climate models rely on parameterizations developed for mid-latitude conditions to handle Arctic turbulent boundary layer processes.
This thesis focuses on modified representation of the Arctic atmospheric processes and understanding their resulting impact on large-scale mid-latitude atmospheric circulation within climate models. The improved turbulence parameterizations, recently developed based on Arctic measurements, were implemented in the global atmospheric circulation model ECHAM6. This involved modifying the stability functions over sea ice and ocean for stable stratification and changing the roughness length over sea ice for all stratification conditions. Comprehensive analyses are conducted to assess the impacts of these modifications on ECHAM6's simulations of the Arctic boundary layer, overall atmospheric circulation, and the dynamical pathways between the Arctic and mid-latitudes.
Through a step-wise implementation of the mentioned parameterizations into ECHAM6, a series of sensitivity experiments revealed that the combined impacts of the reduced roughness length and the modified stability functions are non-linear. Nevertheless, it is evident that both modifications consistently lead to a general decrease in the heat transfer coefficient, being in close agreement with the observations.
Additionally, compared to the reference observations, the ECHAM6 model falls short in accurately representing unstable and strongly stable conditions.
The less frequent occurrence of strong stability restricts the influence of the modified stability functions by reducing the affected sample size. However, when focusing solely on the specific instances of a strongly stable atmosphere, the sensible heat flux approaches near-zero values, which is in line with the observations. Models employing commonly used surface turbulence parameterizations were shown to have difficulties replicating the near-zero sensible heat flux in strongly stable stratification.
I also found that these limited changes in surface layer turbulence parameterizations have a statistically significant impact on the temperature and wind patterns across multiple pressure levels, including the stratosphere, in both the Arctic and mid-latitudes. These significant signals vary in strength, extent, and direction depending on the specific month or year, indicating a strong reliance on the background state.
Furthermore, this research investigates how the modified surface turbulence parameterizations may influence the response of both stratospheric and tropospheric circulation to Arctic sea ice loss.
The most suitable parameterizations for accurately representing Arctic boundary layer turbulence were identified from the sensitivity experiments. Subsequently, the model's response to sea ice loss is evaluated through extended ECHAM6 simulations with different prescribed sea ice conditions.
The simulation with adjusted surface turbulence parameterizations better reproduced the observed Arctic tropospheric warming in vertical extent, demonstrating improved alignment with the reanalysis data. Additionally, unlike the control experiments, this simulation successfully reproduced specific circulation patterns linked to the stratospheric pathway for Arctic-mid-latitude linkages. Specifically, an increased occurrence of the Scandinavian-Ural blocking regime (negative phase of the North Atlantic Oscillation) in early (late) winter is observed. Overall, it can be inferred that improving turbulence parameterizations at the surface layer can improve the ECHAM6's response to sea ice loss.
The wide distribution of location-acquisition technologies means that large volumes of spatio-temporal data are continuously being accumulated. Positioning systems such as GPS enable the tracking of various moving objects' trajectories, which are usually represented by a chronologically ordered sequence of observed locations. The analysis of movement patterns based on detailed positional information creates opportunities for applications that can improve business decisions and processes in a broad spectrum of industries (e.g., transportation, traffic control, or medicine). Due to the large data volumes generated in these applications, the cost-efficient storage of spatio-temporal data is desirable, especially when in-memory database systems are used to achieve interactive performance requirements.
To efficiently utilize the available DRAM capacities, modern database systems support various tuning possibilities to reduce the memory footprint (e.g., data compression) or increase performance (e.g., additional indexes structures). By considering horizontal data partitioning, we can independently apply different tuning options on a fine-grained level. However, the selection of cost and performance-balancing configurations is challenging, due to the vast number of possible setups consisting of mutually dependent individual decisions.
In this thesis, we introduce multiple approaches to improve spatio-temporal data management by automatically optimizing diverse tuning options for the application-specific access patterns and data characteristics. Our contributions are as follows:
(1) We introduce a novel approach to determine fine-grained table configurations for spatio-temporal workloads. Our linear programming (LP) approach jointly optimizes the (i) data compression, (ii) ordering, (iii) indexing, and (iv) tiering. We propose different models which address cost dependencies at different levels of accuracy to compute optimized tuning configurations for a given workload, memory budgets, and data characteristics. To yield maintainable and robust configurations, we further extend our LP-based approach to incorporate reconfiguration costs as well as optimizations for multiple potential workload scenarios.
(2) To optimize the storage layout of timestamps in columnar databases, we present a heuristic approach for the workload-driven combined selection of a data layout and compression scheme. By considering attribute decomposition strategies, we are able to apply application-specific optimizations that reduce the memory footprint and improve performance.
(3) We introduce an approach that leverages past trajectory data to improve the dispatch processes of transportation network companies. Based on location probabilities, we developed risk-averse dispatch strategies that reduce critical delays.
(4) Finally, we used the use case of a transportation network company to evaluate our database optimizations on a real-world dataset. We demonstrate that workload-driven fine-grained optimizations allow us to reduce the memory footprint (up to 71% by equal performance) or increase the performance (up to 90% by equal memory size) compared to established rule-based heuristics.
Individually, our contributions provide novel approaches to the current challenges in spatio-temporal data mining and database research. Combining them allows in-memory databases to store and process spatio-temporal data more cost-efficiently.
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.