4 ms·
Formal methods, in theory, don't eliminate errors. In practice, though, they do, as dramatically demonstrated by fuzzing CompCert C compiler.
by sanxiyn 9y ago
Formal methods, in theory, don't eliminate errors. In practice, though, they do, as dramatically demonstrated by fuzzing CompCert C compiler.
- aidenn0 9y agoIIRC they were actually able to get CompCert to generate incorrect code when fuzzing due to a bug in a system header file. Formal methods do (both in theory and practice) eliminate errors that can occur within the scope of what they cover. If there is an error in your model for the underlying system, then formal methods don't save you, but it seems obvious that eliminating one source of bugs reduces overall bugs. Furthermore, if there is an error for your formal model for the underlying system, there would also probably be an error with your informal model that your programmers would have in their head while developing software without formal methods, yielding similar bugs. All software should be tested; that doesn't mean formal methods have no value.