[berlinquin]

First time reading about compiler fuzzing, but seems like there's some parallels with TLA+.

With TLA+, you could check a compiler's specification before you implement it. Then, once you've implemented it, you could do fuzzing on the actual program.

I wonder how much overlap there is between bugs you could catch with TLA+ vs fuzzing.

[ahelwer]

The term you're looking for is model-based testing, where a formal description of the system is used to generate sequences of events which are fed as input to the system under test; the SUT state is then checked for equivalence to the model state. There is significant overlap in concept between model-based testing, property-based testing, and fuzzing: all involve the structured (some more, some less) generation of random inputs to a SUT and the checking of SUT behavior against an assumed-correct oracle. This spans from feeding random system files to the program to see whether it crashes with a strange exception, to a more formalized process directed by a TLA+ (or other language) spec as you've described.

[berlinquin]

Thanks for naming "model-based testing"--added to my vocabulary. I was thinking more about this, and I would expect very little overlap in the bugs that you could expect to catch with model-based testing vs. fuzzing.

For example, if I get an error with TLA+--e.g. some state reaches deadlock, or there's an invariant that's violated by some behavior--it takes me a good deal of interpretation to see if there's actually a problem, or if just need to update my spec.

With fuzzing, it seems like the errors would be pretty clear to interpret. e.g. uncaught exceptions, or out-of-bounds memory accesses are clear problems with an implementation, and I would think takes less interpretation.

[pfdietz]

Another approach to compiler fuzzing is blackbox differential fuzzing. Generate random valid programs and see if they do the same thing with different compiler settings, or even with two or more different compilers. This does mean you need to generate valid programs, which present challenges in languages with undefined or implementation-specific behaviors.

This is blackbox, so it doesn't allow one to start from nothing as a greybox fuzzer would.

Anyway, testing is not like programming in that different approaches are incompatible. Different testing approaches typically have different blind spots, so they complement each other.