Fine-Grained Complexity of Program Verification
Tools to automatic program verification have been a central research topic over the last decades. Often disparaged as slow in the past, the steady enhancement of tools paid off in recent years. In fact, tool-based approaches to verification have proven themselves to be rather efficient and applicable. This development has led to a gap between theory and practice. While tools perform well, verification tasks are still deemed computationally hard by classical complexity theory. This has two reasons. On the one hand, tools identify and exploit structures that are characteristic for practical instances. On the other hand, worst-case complexity relies on artificial instances that do not occur in practice. In order to bridge the gap, we employ Parameterized and more specific Fine-Grained Complexity to tackle the latter reason. The problem with classical complexity theory is that its measurements are solely based on the size of an instance. Structural characteristics and parameters are ignored. Parameterized complexity takes additional parameters of an instance into account and generates a finer picture of the complexity of a problem. It allows for measuring time and space requirements in terms of these parameters. Fine-grained complexity even goes one step further and proves the optimality of obtained algorithms. We provide an interdisciplinary study connecting program verification and parameterized complexity. To this end, we conducted several fine-grained complexity analyses of typical tasks from the spectrum of program verification. This includes classical safety verification problems like bounded context switching and its variants, safety and liveness verification problems for parameterized systems, as well as consistency testing problems for shared memories. Our main findings are new and provably optimal verification algorithms for each of the considered problems. These reveal the precise time requirements for solving these tasks. Moreover, we provide new hardness results that distinguish between tractable and intractable parameters. Altogether, our study shows that program verification greatly benefits from the algorithmic techniques and lower bound frameworks provided by parameterized and fine-grained complexity. Our results contribute to understanding the complexity of the considered verification tasks in more detail and ultimately help to identify simple and hard instances.
Tools zur automatisierten Verifikation von Programmen sind schon seit einigen Jahrzehnten zentraler Gegenstand der Forschung. In der Vergangenheit oft als langsam erachtet, hat sich das Bild über Verifikationstools jedoch aus heutiger Sicht gewandelt. Die stetige Weiterentwicklung tool-basierter Ansätze hat dazu geführt, dass sich selbige als sehr effizient und einfach anwendbar erwiesen haben. Dies führte jedoch unweigerlich zu einer Diskrepanz zwischen Theorie und Praxis. Während Verifikationstools verlässlich und effizient Programme auf ihre Korrektheit überprüfen, gelten die zugrundeliegenden Verifikationsaufgaben immer noch als sehr rechenaufwendig. Dies hat zwei Gründe. Einerseits nutzen Tools strukturelle Eigenschaften, die typisch für Instanzen aus der Praxis sind, aus, um das implementierte Verifikationsverfahren zu beschleunigen. Andererseits basiert die Worst-Case-Komplexität von Verifikationsaufgaben auf künstlichen Instanzen, die in der Praxis ohnehin nicht vorkommen. Mit dieser Arbeit leisten wir einen ersten Beitrag zur Aufhebung dieser Diskrepanz. Dazu nutzen wir zwei neue Arten von Komplexitätstheorien, die bei letzterem Grund für obige Diskrepanz ansetzen: nämlich die Parametrisierte Komplexitätstheorie und die sogenannte Feingranulare Komplexitätstheorie. Das Problem der klassischen Komplexitätstheorie ist, dass ihre Messungen ausschließlich auf der Eingabegröße einer Instanz beruhen. Strukturelle Besonderheiten und Parameter werden jedoch ignoriert. Parametrisierte Komplexitätstheorie misst Zeit- und Platzbedarf in Abhängigkeit dieser Parameter und bietet daher ein deutlich detaillierteres Bild der Komplexität eines Problems. Mit feingranularer Komplexitätstheorie ist es sogar möglich, zu beweisen, dass ein gefundener Algorithmus für das zugrundeliegende Problem optimal ist bezüglich Zeit- oder Platzverbrauch. Diese Arbeit umfasst eine interdisziplinäre Studie, die Programmverifikation und parametrisierte Komplexitätstheorie vereint. Gegenstand der Studie sind mehrere feingranulare Komplexitätsanalysen von Problemen, die dem Spektrum der Programmverifikation zugeordnet werden. Dazu gehören klassische Probleme wie Bounded Context Switching und Variationen davon, sowie Safety- und Liveness-Verifikationsprobleme für parametrisierte Systeme und Testing-Probleme für verteilte Speicher. Die wichtigsten Ergebnisse sind neue, optimale, Verifikationsverfahren für jedes der betrachteten Probleme. Diese lösen die betrachteten Verifikationsproblem in der genau dafür benötigten Zeit. Zudem beweisen wir neue Hardness-Resultate, die zwischen effizient nutzbaren und übrigen Parametern unterscheiden. Unsere Studie zeigt, dass Programmverifikation von algorithmischen Techniken und Frameworks für untere Schranken, die aus der parametrisierten Komplexitätstheorie bekannt sind, profitieren kann. Die Ergebnisse tragen dazu bei, die Komplexität von Verifikationsproblemen genauer zu verstehen und helfen letztlich, einfache und schwierige Instanzen zu unterscheiden.
Preview
Cite
Access Statistic
Rights
Use and reproduction:
