A fundamental concept in analyzing infinite-state systems (such as programs) is that of abstraction. Often, a system may be converted to a simpler abstract form where certain questions are decidable, such that proofs in the abstract system carry over to proofs in the original system. Abstract interpretation is a framework for mathematically describing program abstraction and their meaning. A basic step in the process is the creation of abstract transformers: each statement in the original program must be translated to a corresponding abstract statement. [0]

[0] Ball, Thomas, Shuvendu K. Lahiri, and Madanlal Musuvathi. “Zap: Automated theorem proving for software analysis.” International Conference on Logic for Programming Artificial Intelligence and Reasoning. Springer, Berlin, Heidelberg, 2005.