Research Progress on Abstract Interpretation and Its Application

Abstract interpretation is a theory of abstraction and approximation of the mathematical structures used in the formal description of complex systems and the inference or verification of their properties. Since being proposed in 1970 s, abstract interpretation has been widely applied to many fields, including semantic models, program analysis and verification, verification of hybrid systems, program transformation, analysis of systems biology models, etc. In recent years, abstract interpretation has made great progress in program analysis, neural network verification, completeness reasoning, improvement of abstract domains, etc. Based on this, we systematically review the research progress of abstract interpretation and its applications. Firstly, we outline the basic concepts of abstract interpretation theory, and review the recent research progress of abstract interpretation theory and abstract domains; then, we review the recent research progress in abstract interpretation-based program analysis, verification and robust training of neural networks, analysis of deep learning programs; after that, we also review the progress of some other applications of abstract interpretation, including trustworthiness assurance of smart contract, information security, and quantum computing; At last, potential future directions in the field of abstract interpretation are pointed out.