If I understand correctly, modeling a program at the x86 instruction set level is cool but it would have a more complicated list of states than a high level lan

If I understand correctly, modeling a program at the x86 instruction set level is cool but it would have a more complicated list of states than a high level language. More states means more computation to do the symbolic execution, therefore it is harder to optimize well enough to get useful results on large programs. The intro implies that the main motivation for doing this on x86 instructions is uncertainty that a high-level language's abstraction is faithfully translated into x86 instructions. I recognize that this language->assembly conversion was accepted to be correct as a basic assumption when I did graduate work in validation techniques. I think there are some PL theorists that have more rigorous mathematical proofs for their compilers, but I'm not sure how many of those get all the way down to the x86 instruction set.