Speaker: Klaus Havelund

Title: Fuzz Testing with Temporal Constraints

Abstract: Testing is in practice commonly performed by executing carefully planned scripts, which exercise particular planned scenarios. Fuzz testing can be applied as a complementary approach, to exercise a system outside the boundaries of the expected. Fuzz testing, however, can be too random. In this work we explore an approach to fuzz testing using an expressive temporal logic named MaTL (Matching Temporal Logic) for expressing constraints on tests, restricting generated tests to only such that satisfy the provided constraints. MaTL is a linear temporal logic supporting future and past time operators, and a matching construct that selects argument values from events, similar to pattern matching in functional programming languages. This construct is related to the freeze operator. Constraint solving is performed using an SMT solver.