Tests beweisen nicht, dass zwei Funktionen �quivalent sind. Das hier schon.
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…