It's interesting that VW cars have been taken off the road for unintended acceleration. Also that quickcheck was used to find many timing related bugs between software components that VW uses. It was used after the models were taken off the road. There are other models still not recalled using similar software from the same era.