Validating system properties exhibited in execution traces.