Paper accepted at TACAS'16