Software specialization via symbolic execution