UninterpretedFunctions are equivalent to Abstract Functions, but used in a theoretical framework. You can think of it as a function place holder because it is an undefined or "uninterpreted" function.
"Suppose that instead of specifying the exact function of the ALU in our abstract model, we simply use a symbol f to denote this function. Suppose further that we use the same function symbol in our implementation, and we are able to prove a refinement relation between the two. It would then follow that the refinement holds for any concrete function we might want to plug in place of f." - http://www.mimuw.edu.pl/~sl/teaching/PMW/SMV-doc/tutorial/node32.html