Scalable verification techniques for data-parallel programs