Fuzz Testing with Temporal Constraints.

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. However, fuzz testing 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 that supports future and past time operators and a match construct that selects argument values from events, similar to pattern matching in functional programming languages. Constraint solving is performed using the Z3 SMT solver.