Model-free Stateful Random Testing

Abstract

Property-based testing (PBT) has enabled greater confidence in the correctness of programsand facilitated formal verification by exposing false theorems earlier in the proving process. However, most PBT libraries are designed for pure programs, even though much critical software such as systems software are stateful. Current stateful PBT libraries generally require the programmer to implement a model of the program under test, increasing developer overhead and introducing another source of error. In this thesis, I aim to significantly reduce developer overhead when testing stateful programs. I introduce seq-test, a tool for testing stateful C programs that eliminates the need for models. seq-test is embedded in CN, a specification language for formally verifying C programs. Test generation uses a generation-by-execution strategy, where CN preconditions are used to discard illegal call sequences, and CN postconditions are used to detect bugs. We also implement two- phase shrinker to increase the usability of generated falsifying examples in debugging. Finally, I evaluate the bug-finding ability of seq-test against AFL++, a popular fuzzer, and Bennet, a PBT tool embedded in CN, on a variety of case studies.