Fuzz Testing with Temporal Constraints

Testing is in practice commonly performed by executing care-fully planned scripts, which exercise particular planned scenarios. Fuzztesting can be applied as a complementary approach, to exercise a systemoutside the boundaries of the expected. However, fuzz testing can be toorandom. In this work, we explore an approach to fuzz testing using anexpressive temporal logic named MaTL (Matching Temporal Logic) forexpressing constraints on tests, restricting generated tests to only suchthat satisfy the provided constraints. MaTL is a linear temporal logicthat supports future and past time operators and a match constructthat selects argument values from events, similar to pattern matchingin functional programming languages. Constraint solving is performedusing the Z3 SMT solver.