Title: Methods and tools for the formal verification of software : an analysis and comparison
Language: English
Authors: Rainer-Harbach, Marian 
Qualification level: Diploma
Advisor: Salzer, Gernot
Issue Date: 2011
Number of Pages: 125
Qualification level: Diploma
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.
Diese Arbeit gibt einen Überblick über einige theoretische Aspekte von formaler Verifikation. Mehrere Tools werden ausführlich beschrieben.
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.

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.
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.
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.
Keywords: Formale Verifikation; Formale Methoden; Software; Qualitätssicherung; Verifikationstools
formal verification; formal methods; software; quality assurance; verification tools
URI: https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-45918
http://hdl.handle.net/20.500.12708/10655
Library ID: AC07812010
Organisation: E185 - Institut für Computersprachen 
Publication Type: Thesis
Hochschulschrift
Appears in Collections:Thesis

Files in this item:


Page view(s)

12
checked on Jul 20, 2021

Download(s)

79
checked on Jul 20, 2021

Google ScholarTM

Check


Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.