[Back]


Diploma and Master Theses (authored and supervised):

I. Feinerer:
"Formal Program Verification: A Comparison of Selected Tools and Their Theoretical Foundations";
Supervisor: G. Salzer; E 185 Institut für Computersprachen, 2005; final examination: 2005-02-03.



English abstract:
Formal specification and verification of software have made small but continuous advances throughout its long history, and have reached a point where commercial tools became available for verifying programs semi-automatically or automatically.

The aim of the master thesis is to evaluate commercial and academic verification tools with respect to their usability in developing software and in teaching formal methods. The thesis will explain the theoretical foundation and compare the capabilities and characteristics of selected commercial and academic tools on concrete examples.

The theoretical foundations deal on the one hand with the general ideas and principles of formal software verification, on the other hand present some internals of the selected tools to give a comprehensive understanding.

The discussed tools are the Frege Program Prover, KeY, Perfect Developer, and the Prototype Verification System. The examples encompass simple standard computer science problems. The evaluation of these tools concentrates on the whole development process of specification and verification, not just on the verification results.

German abstract:
Formale Spezifikation und Verifikation sind durch die durch kontinuierliche Weiterentwicklung in letzter Zeit an einem Punkt angelangt, wo Programme beinahe automatisch verifiziert werden können.

Das Ziel dieser Magisterarbeit ist es, sowohl kommerzielle als auch für wissenschaftliche Zwecke entwickelte Verifikationsprogramme zu testen. Der Hauptaugenmerk liegt auf dem Nutzen dieser Werkzeuge in der Software-Entwicklung und in der Lehre. Hierzu wird diese Magisterarbeit die theoretischen Grundlagen vorstellen und auf die verschiedenen Fähigkeiten und Eigenheiten der ausgewählten Werkzeuge eingehen.

Die theoretischen Grundlagen behandeln einerseits Ansätze, die für die formale Verifikation gebraucht werden, andererseits wird die Funktionsweise der ausgewählten Werkzeuge erklärt.

Die begutachteten Programme sind der Frege Program Prover, KeY, Perfect Developer und das Prototype Verification System. Die Beispiele, mit denen diese Werkzeuge getestet werden, sind typische Problemstellung der Informatik. Bei der Evaluation wird auf den ganzen Ablauf beim Einsatz dieser Werkzeuge eingegangen und nicht nur auf das Endergebnis.

Keywords:
Formal program verification


Electronic version of the publication:
http://publik.tuwien.ac.at/files/pub-inf_4115.pdf


Created from the Publication Database of the Vienna University of Technology.