Imperative Programmiersprachen sind in der modernen Softwareentwicklung allgegenwärtig, ihre Verwendung von veränderbaren Variablen und Objekten stellt aber ein Problem für formale Softwareverifikation dar. Programme in diesen Sprachen können normalerweise nicht direkt auf die unveränderliche Welt von Logik und Mathematik zurückgeführt werden, sondern müssen in eine explizit modellierte Semantik der jeweiligen Sprache eingebettet werden. Diese Indirektion erschwert den Einsatz von interaktiven Theorembeweisern, da sie die Entwicklung von neuen Werkzeugen, Taktiken und Logiken für diese "innere" Sprache bedingt. Die vorliegende Arbeit stellt einen Compiler von der imperativen Programmiersprache Rust in die pur funktionale Sprache des Theorembeweisers Lean vor, der nicht nur generell das erste allgemeine Werkzeug zur Verifikation von Rust-Programmen darstellt, sondern dies insbesondere auch mithilfe der von Lean bereitgestellten Standardwerkzeuge und -logik ermöglicht. Diese Transformation ist nur möglich durch spezielle Eigenschaften von (der "sicheren" Teilsprache von) Rust, die die Veränderbarkeit von Werten auf begrenzte Geltungsbereiche einschränken und statisch durch Rusts Typsystem garantiert werden. Die Arbeit demonstriert den Einsatz des Compilers anhand der Verifikation von Realbeispielen und zeigt die Erweiterbarkeit des Projekts über reine Verifikation hinaus am Beispiel von asymptotischer Laufzeitanalyse auf. 

Veröffentlichungen

Veröffentlichung

Simple Verification of Rust Programs via Functional Purification

Betreuer

Lehrstuhlinhaber
Prof. Gregor Snelting

Studenten

Ehemalige Mitarbeiter
Dr.-Ing. Sebastian Ullrich