4 ms·
There's a difference, though: QuickCheck randomly tries a large-ish number of possible inputs to try and disprove a postcondition, whereas formal methods prove
by grandpa 12y ago
There's a difference, though: QuickCheck randomly tries a large-ish number of possible inputs to try and disprove a postcondition, whereas formal methods prove the postcondition for all inputs. Practically, if the number of possible inputs is huge compared to the number of failure cases, it's unlikely that QuickCheck will find it. I strongly suspect - and this would be an interesting experiment - that QuickCheck wouldn't have found this particular bug, since Timsort has been in use for years without anyone noticing it.
- TheLoneWolfling 12y agoWhat about AFL?
- jamesfisher 12y agoWhat's AFL?
- fpgaminer 12y agoAmerican Fuzzy Lop (http://lcamtuf.coredump.cx/afl/ http://lcamtuf.coredump.cx/afl/), a fuzzer which instruments programs at compile-time to help find interesting inputs faster than brute-force fuzzing. It may have indeed found a bug in TimSort, since it's more apt at exercising branches, but I think AFL is C/C++ only.
- deleted 12y ago[deleted]