Methods and tools for the formal verification of software : an analysis and comparison

Abstract

Die Aufgabenstellung, die Korrektheit von Software zu beweisen (Formale Verifikation), ist seit vielen Jahren Forschungsthema. Trotzdem ist die Nutzung von formalen Methoden in der Praxis noch nicht weit verbreitet. Ein zentraler Grund dafür ist der Mangel an leicht zugänglichen, aber trotzdem leistungsstarken Tools, die Softwareentwickler bei dieser komplexen Aufgabe unterstützen. In den letzten Jahren ist eine neue Generation von Tools erschienen: Sie zielen auf die Verifikation von Programmen ab, die in Programmiersprachen wie C und Java geschrieben sind und erheben den Anspruch, auch für Softwareentwickler ohne Ausbildung in formalen Methoden verwendbar zu sein.<br />Diese Arbeit gibt einen Überblick über einige theoretische Aspekte von formaler Verifikation. Mehrere Tools werden ausführlich beschrieben.<br />Einige davon werden ausgewählt, um ihre Fähigkeiten in einem praktischen Vergleich zu beweisen. Dazu werden Beispiele verwendet, die auf häufig vorkommenden Problemstellungen basieren. Einige allgemeine Anforderungen an Verifikationstools in Industrie und Lehre werden ebenfalls diskutiert. Die in dieser Arbeit analysierten Tools sind CBMC, Escher C Verifier, Frama-C/Jessie, Frege Program Prover, KeY, Perfect Developer, Prototype Verification System, VCC und VeriFast.<br />

The task of proving the correctness of software (formal verification) has been a research topic for many years. Despite that, formal methods still have not been widely adopted in practical areas. A key reason for this has been the lack of accessible yet powerful tools that are able to efficiently support the software engineer in this complex exercise. In the last few years, a new generation of tools has appeared: They are aimed at the verification of programs written in programming languages such as C or Java and claim to be usable by software engineers without education in formal methods.<br />This thesis gives an overview of some theoretical aspects of formal verification. A number of tools is extensively described, and some of them are selected to compete in a practical comparison. The comparison is based on tasks that are commonly encountered in software development.<br />Some general thoughts on requirements for formal verification tools in industry and teaching are also given. The tools analyzed are CBMC, Escher C Verifier, Frama-C/Jessie, Frege Program Prover, KeY, Perfect Developer, Prototype Verification System, VCC and VeriFast.<br />