Haltermann, Jan Frederik (2025) Cooperative Software Verification. PhD, Universität Oldenburg.

Preview

Volltext (2867Kb)

Abstract

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.

["eprint_fieldname_title_plus" not defined]

Kooperative Softwareverifikation

["eprint_fieldname_abstract_plus" not defined]

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.

Item Type:	Thesis (PhD)
Uncontrolled Keywords:	Software Verification, Black-Box-Cooperation, Invariant Generation, Ranged Program Analysis, Verification Artifact, Decomposition
Subjects:	Generalities, computers, information > Computer science, internet
Divisions:	School of Computing Science, Business Administration, Economics and Law > Department of Computing Science
Date Deposited:	16 May 2025 11:29
Last Modified:	16 May 2025 11:29
URI:	https://oops.uni-oldenburg.de/id/eprint/7188
URN:	urn:nbn:de:gbv:715-oops-72698
DOI:
Nutzungslizenz:

Actions (login required)

View Item