Program verification techniques based on the abstract interpretation theory

Abstract

The abstract interpretation theory was proposed by P. Cousot and R. Cousot in 1977, and is widely used in the program's static analysis domain to construct and approximate the program's fixpoint semantics. This paper describes the abstract interpretation framework of the program semantics based on the Galois connection, and then discusses three typical applications of the abstract interpretation theory: The program transformation, the program verification techniques about the safety property and the program verification techniques about the liveness property. Finally, it points out the main directions of the program verification techniques based on the abstract interpretation theory.