Data flow in program verification

Abstract: We present several techniques and insights that aid program verification. The common theme of these techniques and insights is their relation to the notion of data flow. Intuitively, there is a data flow from program statement s to program statement s' if s writes a value (to memory) that s' uses (reads from memory). This notion induces a particular view on a program that is to be verified. For example, when we want to find out which values a certain variable in a certain statement can assume in a program, it is natural to check all the incoming data flows for that variable in that statement and see which values they provide. Of course, the provided values may depend on other data flows and so on. There is a wide variety of ways to apply this view on programs in program verification. For this thesis, we picked the following three questions. 1. The analogue to classical Floyd proofs in the data flow view are data flow proofs. What is their potential and what are their limitations? 2. Data flow becomes much more complex in the presence of arrays. Can we develop a scalable abstract domain that is powerful enough to find a good approximation of the data flow relationships in a program with arrays? 3. The absence of data flows in a program with arrays (i.e., the independence of certain statements) is often an essential and difficult part of the program’s correctness proof. Can we give a program transformation that encodes this information into the transformed program in order to relieve some backend-verifier of these proof tasks? In this thesis we will give answers to these three questions
Abstract: Gegenstand dieser Arbeit ist die theoretische und praktische Untersuchung von Techniken, die die Verfikation von Programmen unterstützen sollen. Den vorge- stellten Techniken gemeinsam ist, dass ihnen das Konzept des Datenflusses zu- grundeliegt. Zwischen Programmbefehl s und Programmbefehl s' besteht ein Da- tenfluss, wenn s einen Wert in den Speicher schreibt, den s' verwendet (also aus dem Speicher liest). Dieses Konzept legt eine bestimmte Sicht auf das zu verifizie- rende Programm nahe. Wenn man zum Beispiel herausfinden will, welche Werte eine bestimmte Variable in einem bestimmten Programmbefehl annehmen kann, dann scheint es natürlich, alle eingehenden Datenflüsse zurückzuverfolgen, um her- auszufinden, mit welchen Werte die Variable geschrieben worden sein kann. Diese Werte können ihrerseits wiederum von anderen Variablen abhängen, sodass weite- re Datenflüsse zurückverfolgt werden müssen, bis alle möglichen Werte ermittelt werden können. Es gibt ein breites Spektrum von Möglichkeiten, diese Sicht auf Programme zu deren Verifikation einzusetzen. Die folgenden drei Fragen bilden einen Auszug aus diesem Spektrum: 1. Ein Analogon zu klassischen Floyd-Beweisen sind Daten- flussbeweise. Was sind die Vor- und Nachteile von Datenflussbeweisen? 2. Durch die Anwesenheit von Arrays im Programm wird es deutlich schwieriger, eine gu- te Charakterisierung der im Programm möglichen Datenflüsse zu ermitteln. Gibt es eine abstrakte Domäne (im Sinne der abstrakten Interpretation von Program- men), die gut skaliert und mächtig genug ist, um eine nützliche Approximation der Datenflüsse in einem Programm mit Arrays herzuleiten? 3. Die Abwesenheit von bestimmten Datenflüssen in einem gegebenen Programm mit Arrays (und die daraus resultierende Unabhängigkeit der zugehörigen Programmbefehle) ist häufig ein wichtiger und schwer zu inferierender Bestandteil des Korrektheitsbeweises des Programms. Ist es möglich eine Programmtransformation zu entwerfen, die diese Information (über die Abwesenheit von Datenflüssen) in das transformierte Pro- gramm enkodiert, sodass die anschließende Verifikation des Programms diese Be- weisaufgaben nicht mehr zu erledigen braucht? Diese drei Fragen sollen in dieser Arbeit beantwortet werden

Object Details

• Location: Deutsche Nationalbibliothek Frankfurt am Main
• Extent: Online-Ressource
• Language: Englisch
• Notes: Universität Freiburg, Dissertation, 2019

Classification and Topics

• Keyword: Verifikation ; Programmierung ; Formaler Beweis ; Software

Contributors, Places and Time

• Event: Veröffentlichung
• (where): Freiburg
• (who): Universität
• (when): 2020
• Creator: Nutz, Alexander
• Contributor: Podelski, Andreas ; Albert-Ludwigs-Universität Freiburg. Fakultät für Angewandte Wissenschaften

Further information

• DOI: 10.6094/UNIFR/165473
• URN: urn:nbn:de:bsz:25-freidok-1654737
• Rights: Der Zugriff auf das Objekt ist unbeschränkt möglich.
• Last update: 14.08.2025, 10:52 AM CEST