3 ms·
A point they're implicitly making is: it's harder to apply formal methods retrospectively. The state of the art in formal verification involves writing the proo
by dgacmu 3y ago
A point they're implicitly making is: it's harder to apply formal methods retrospectively. The state of the art in formal verification involves writing the proofs jointly with the code in a language designed for verification, such as Dafny (earlier), F*, or VeRus (emerging).
Fuzzing is much easier to add to an existing system - though even there, there's a lot of benefit from designing for testability.
- rurban 3y agoSorry, the state of the art of formal verification is proving C, C++ or Java code directly. Everything else is lost in translation. You just to mark some variables as symbolized and bound the loops. cbmc
- dgacmu 3y agoNot really. Cbmc is really cool but it doesn't lead to the kind of high level proof refinement that lets you say things like "this low level code correctly implements the paxos protocol". Cmbc is -useful- and lets you check some important safety properties and it's a great tool. But it's not the state of the art in terms of how extensively you can check things with formal verification. It's closer to the state of the art of what you can do with legacy code. Things like VeRus let you write annotated rust together with proofs that can show higher-level properties such as liveness, mutual exclusion, etc.