Research On Generation Of Invariant Based On Abstract Interpretation

Abstract interpretation provides a general framework to generate program invariants automatically.However,most existing numerical abstract domains under this framework can only express constraint sets that are convex geometrically.Therefore,using convex abstract domains to analyze special program structures involving disjunctive semantics(whose constraint sets are non-convex)may lead to imprecise results.In this paper,we go deeply into abstract interpretation in this thesis,and present a novel approach using loop decomposition and deduction to assist the analysis of abstract interpretation for loop structures with explicit and implicit disjunctive semantics respectively.The method is committed to alleviate the problem of great semantic loss and improve the accuracy of the resulting invariants.The main work is as follows:(1)In the aspect of semantics-based program analysis,we introduce the definition equation conversion system and its important role in the formal analysis.We conduct the study on constructing the equation system of the C language program.The minimum fixed point and semantic lattice theory are introduced.We analysis the incalculable nature of equation system without abstract interpretation.(2)In terms of the abstract interpretation,we introduce the basic concepts of abstract interpretation-related research and study the general methods and theories of abstract interpretation.The construction process and expression from of general abstract domains is summarized as well.Besides,we researched and concluded the three problems faced by abstract interpretation,i.e.the optimization of abstract interpretation itself,the construction of the complex abstract domains and the loss of semantic of the special program structure.The causes?effects and the representative works of the three problems are studied.Finally,the application of abstract interpretation in the program analysis and verification.(3)Detailed analysis is conducted on the problem of the semantic loss when abstract interpreting for program structures with explicit and implicit disjunctive semantics.To address this problem,we proposed a novel approach using loop decomposition and deduction to optimize the analysis on the program structure with explicit and implicit disjunctive semantics.The approach reduces the value of redundancy and is closer to the real semantics,thereby generating more accurate invariants,and benefit some security properties reasoning.(4)Based on the improved method,we implement an automated invariant generation tool named InvImpr and evaluate it.Compared with existing approaches,the experimental results show that our approach can generate more precise invariants without too much time cost for loop structures involving disjunctive semantics,which is also helpful for reasoning about some security properties.