3 ms·
Can't you brute-force correctness, by literally trying each and every possible input and output, and literally trying every possible state? No. Take a simple
by caf 10y ago
Can't you brute-force correctness, by literally trying each and every possible input and output, and literally trying every possible state?
No.
Take a simple function that has two 64-bit numbers as input and one output; your sixteen 4Ghz cores would take over 11 billion times the current age of the universe to verify it.
You can, instead, do things like symbolic execution... and it turns out, that kind of thing is often a big part of "formally proven correct".
- logicallee 10y agoWhat do fuzzers do in practice? (I am not up on the state of the art)? They try to explore edge cases, but how do they know what is likely to be an edge case? Or how do they try to get coverage of their fuzzing?
- cnvogel 10y agoThey no longer just try out random combinations or cover the input space exhaustively (which is not feasible anyway). Nowadays they use instrumentation in the fuzzed/tested code to have guidance in what direction the input should be modified to get more cases the code covered. Good example: http://lcamtuf.coredump.cx/afl/ http://lcamtuf.coredump.cx/afl/
- caf 10y agoOne common technique (used by eg. AFL) is to instrument the program under test, so it can see when a different codepath has been triggered.