Let's say I have a program
P, in form of a binary code for x86 architecture.
I want to find a Boolean formula F (in form of CNF, or something like that), such that
F(input,output) = true iff P(input) = output
So to answer a question "what output does the program produce on given input" I will only need to run a SAT/SMT solver for
X on formula
F(input,X) == true.
I understand that this problem is undecidable in general case, but I only care for some practical cases.
What keywords should I google to find more about this topic?