Paper accepted at TACAS'17