This thesis explores the adoption of two established specification patterns within the Rust verifier Creusot: type invariants and ghost code. Type invariants empower users to attach logical predicates to data types, which Creusot enforces for all values of a type. Ghost code enables auxiliary constructs that bolster verification without affecting the program's runtime behavior. Especially when employed in tandem, these patterns enhance the expressivity of specifications and ensure the scalability of Rust verification. We introduce an innovative framework for type invariants, including its implementation in Creusot. Moreover, we scrutinize Creusot's current implementation of ghost code, identifying soundness deficiencies and presenting refinements to address them. Our evaluation demonstrates that these extensions not only facilitate more concise program specifications but also maintain robust verifiability.     «

This thesis explores the adoption of two established specification patterns within the Rust verifier Creusot: type invariants and ghost code. Type invariants empower users to attach logical predicates to data types, which Creusot enforces for all values of a type. Ghost code enables auxiliary constructs that bolster verification without affecting the program's runtime behavior. Especially when employed in tandem, these patterns enhance the expressivity of specifications and ensure the scalabi...     »

Diese Arbeit untersucht die Integration von zwei etablierten Spezifikationsmustern in den Rust-Verifizierer Creusot: Typinvarianten und Ghostcode. Typinvarianten ermöglichen es dem Benutzer, Datentypen mit logischen Prädikaten zu versehen, die Creusot für alle Werte eines Typs durchsetzt. Ghostcode ermöglicht Hilfskonstrukte, die die Verifikation unterstützen, ohne das Laufzeitverhalten des Programms zu beeinflussen. Insbesondere in Kombination erhöhen diese Muster die Ausdruckskraft von Spezifikationen und gewährleisten die Skalierbarkeit der Rust-Verifikation. Wir stellen ein innovatives Framework für Typinvarianten vor, einschließlich dessen Implementierung in Creusot. Darüber hinaus analysieren wir die derzeitige Implementierung von Ghost Code in Creusot, identifizieren Soundness-Mängel und stellen Verfeinerungen vor, um diese zu beheben. Unsere Evaluierung zeigt, dass diese Erweiterungen nicht nur präzisere Programmspezifikationen ermöglichen, sondern auch eine robuste Verifizierbarkeit gewährleisten.     «

Diese Arbeit untersucht die Integration von zwei etablierten Spezifikationsmustern in den Rust-Verifizierer Creusot: Typinvarianten und Ghostcode. Typinvarianten ermöglichen es dem Benutzer, Datentypen mit logischen Prädikaten zu versehen, die Creusot für alle Werte eines Typs durchsetzt. Ghostcode ermöglicht Hilfskonstrukte, die die Verifikation unterstützen, ohne das Laufzeitverhalten des Programms zu beeinflussen. Insbesondere in Kombination erhöhen diese Muster die Ausdruckskraft von Spez...     »