4 posts
Bounded Model Checker wie Kani und relationale Model Finder wie Alloy ermöglichen die Verifikation von Eigenschaften mit gewöhnlichen Assertions und Constraints. Sie geben Liveness-Beweise auf, dafür ist die Lernkurve auf Stunden statt Wochen gemessen.
Sie müssen keine lineare temporale Logik lernen, um einen Model Checker zu verwenden. Tools wie Kani, CBMC und Alloy ermöglichen die Verifikation von…
Model-Checking-Tools wie Kani erlauben es, Rust-Eigenschaften mit Assertions statt formaler Beweise zu verifizieren. Das Problem ist, was passiert, wenn deine Schleifen keine kleinen Grenzen haben.
Man kann Rust-Code korrekt beweisen, ohne einen einzigen Beweis zu schreiben. Das Tool, das das macht, heißt Model Checker, und für Rust ist der praktischste…
Differential Testing hilft dir, Bugs zu finden, ohne die korrekte Antwort zu kennen. Das Problem ist, dass korrelierte Fehler wie Übereinstimmung aussehen. So entdeckst du die blinden Flecken.
Du kannst Differential Testing ohne formalen Beweis vertrauen, aber nur, wenn du genau verstehst, wo es zusammenbricht. Die Schwäche heißt Common-Mode Failure.…
N-version programming setzt voraus, dass deine Implementierungen �bereinstimmen. Wir zeigen, warum Tests nicht ausreichen, wie SMT solver tats�chlich �quivalenz beweisen k�nnen, und wo man die Grenze zwischen gut genug und formal verifiziert zieht.
Du hast ein n-version-System gebaut. Drei unabh�ngige Implementierungen derselben kritischen Funktion, ein Voter, der das Mehrheitsergebnis w�hlt, und ein…