Software plays an important role in our daily lives. To ensure that a program fulfills specific requirements, software verification is used. Cooperative software verification aims to combine the strengths of existing components on a conceptual level so that they work together in a loosely coupled manner to solve a task. This thesis presents a systematic analysis of the effects of using cooperative software verification. We develop and evaluate three concepts for cooperative software verification: The sequential concept, CoVEGI, allows components to cooperate on invariant generation, a core task in software verification. The cyclic concept is based on a decomposition of the widely used CEGAR scheme. In the decomposed version, C-CEGAR, three stateless components cooperate via existing verification artifacts. Finally, we propose the concept of ranged program analysis, which enables the parallel composition of arbitrary verifiers. We experimentally demonstrate the advantages of cooperative verification for each of the three approaches.
Software spielt im Alltag eine wichtige Rolle. Mit Hilfe von Softwareverifikation kann gezeigt werden, dass ein Programm bestimmte Anforderungen erfüllt. Kooperative Softwareverifikation hat das Ziel, die Stärken existierender Ansätze auf einer konzeptionellen Ebene zu kombinieren und diese lose gekoppelt und gemeinsam die Aufgabe lösen zu lassen. In dieser Arbeit wird eine systematische Analyse der Auswirkungen der Verwendung von kooperativer Softwareverifikation durchgeführt. Dafür entwickeln und evaluieren wir drei solche Konzepte: Im sequenziellen Konzept CoVEGI kooperieren Komponenten bei der Invarianten-Generierung – einer Kernaufgabe der Verifikation. Das zyklische Konzept C-CEGAR basiert auf der Zerlegung des CEGAR-Schemas: Drei zustandslose Komponenten kommunizieren über bestehende Verifikationsartefakte miteinander, um die Verifikation durchzuführen. Zuletzt präsentieren wir Ranged Program Analysis, ein Konzept zur parallelen Komposition beliebiger Verifikationswerkzeuge. Die Vorteile jedes der drei kooperativen Ansätze werden experimentell demonstriert.
Software bugs cost developers and companies significant time and money. To help developers find bugs early in the development process, neural bug detectors have been proposed. Neural bug detectors learn from millions of examples to find novel bugs in code. Although effective for simple bugs, they still have many limitations that make them difficult to use in practice. This thesis addresses two key challenges. First, prior work often relied on artificial mutants for training, which do not reflect real bugs. We propose a contextual mutator and mine public repositories for real bug fixes to create more realistic training data. Our evaluation shows that training with this data improves detection of real bugs. Second, current detectors often lack sufficient context, leading to false alarms. We propose an LLM-based validator that leverages extra context to reduce false alarms. Together, these contributions result in a neural bug detector that is significantly more accurate and practical for real-world use.
Softwarefehler kosten Entwicklern und Unternehmen viel Zeit und Geld. Um Fehler früh im Entwicklungsprozess zu finden, wurden Neural Bug Detectors vorgeschlagen. Diese Detektoren lernen aus Millionen von Beispielen, um neue Fehler im Code zu erkennen. Obwohl sie einfache Bugs erkennen können, haben sie noch viele Einschränkungen, die ihre praktische Nutzung erschweren. Diese Arbeit behandelt zwei zentrale Herausforderungen. Erstens basierte frühere Forschung oft auf künstlichen Mutationen, die reale Fehler nur unzureichend abbilden. Daher schlagen wir einen kontextbezogenen Mutationsoperator vor und extrahieren echte „Bug Fixes“ aus öffentlichen Projekten, um realistischere Trainingsdaten zu gewinnen. Unsere Evaluation zeigt, dass das Training auf diesen Daten die Erkennung realer Fehler verbessert. Zweitens fehlt bestehenden Detektoren oft Kontext, was zu Fehlalarmen führt. Wir entwickeln einen LLM-basierten Validator, der zusätzliche Kontext nutzt. Zusammen führen diese Beiträge zu einem neuronalen Fehlerdetektor, der wesentlich genauer und praktikabler für den realen Einsatz ist.
The Practice of Formal Methods 1st ed. 2024. Cham : Springer Nature Switzerland, 2024 (2024), Seite 88-108 1 Online-Ressource(XXVIII, 316 p. 74 illus., 45 illus. in color.)
