Property-Based Testing of Separation Logic Specifications
Separation logic (SL) has been a tried and tested method for specifying the behavior of heap-manipulating programs. We apply property-based testing (PBT) to these specifications for C programs, generating inputs that satisfy preconditions and checking that postconditions hold. Besides providing a specification language...