Property-Based Testing of Separation Logic Specifications

Abstract

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 for testing, using SL means that PBT can act as a stepping stone towards full verification. We have previously developed tools that explore three generation techniques for SL specifications in the fragment supported by the CN verifier. Ongoing and future work develops AustenTest, a standalone tool that uses a separation-logic IR covering a larger SL fragment. AustenTest will be a publicly available, supported tool for other separation-logic verifiers to be able to use. Simultaneously, we are working on applying grammar-based fuzzing as a fourth approach to generation.