Rigorous Linear Programming-Based Numerical Static Analysis

With the wider and wider application of computer,the reliability of software system plays an increasingly important part in many industries.Because of the basic nature of numerical computations,many software systems involve a large number of numerical computations,and many bugs are related to the numerical properties of the programs.Therefore,the analysis of numerical properties of programs such as numerical constraints on variables is very important to ensure the reliability of software system.Abstract interpretation is a theory that can reliably abstract the semantics of programs.This theory provides a static analysis framework for deriving the numerical properties of programs.Under the framework of abstract interpretation,numerical abstract domains are the core of analyzing the numerical properties of programs.Therefore,the accuracy and efficiency of numerical abstract domain are directly related to the accuracy and speed of obtained numerical properties of programs.It is a vital goal that analyzing the numerical properties of programs reliably and efficiently within the allowable range of accuracy error by abstract interpretation.For this end,this paper proposes a new novel rigorous linear programming technique,and combines it with existing rigorous linear programming techniques together to improve the performance of template constraint matrix abstract doamin within the allowable range of accuracy error.Firstly,by leveraging the advantages of floating-point arithmetic in computational efficiency and combining floating-point arithmetic with interval arithmetic together,this paper proposes and implements a novel rigorous linear programming technique which is based on Fourier-Motzkin elimiantion.On the basis,in order to achieve a balance between accuracy and efficiency,this paper proposes heuristic rigorous linear programming technique via combining our novel technique with existing technqiues together,and implements corresponding tool named Rlp Solver whose main idea is choosing a proper rigorous linear programming technqiue automatically to solve linear programming problems according to heuristic rules.Furthemore,this paper conducts contrast experiments between our novel rigorous linear programming technique and existing techniques.Experimental results show that our technique is complementary to existing techniques,and their combination(Rlp Solver)can achieve a better trade-off between cost and precision via heuristic rules.Secondly,this paper constructs and optimizes the template constraint matrix abstract domain based on rigorous linear programming.Because the template constraint matrix abstract domain allows configuring customized template constraint matrix and has polynomial complexity,it has been widely used to derivate the linear constraint relationship of program’s variables.Futher optimization for template constraint matrix abstract domain is of practical significance.As we know,many domain operations of this domain rely on linear programming,therefore the efficiency of linear programming tools is vital for numerical static analysis via this domain.So,in order to improve the performance of template constraint matrix abstract domain,this paper reconstructs this domain by rigorous linear programming.On the basis,this paper builds an experimental platform named RLPAI.On this platform,this paper conducts constrast experiments between this new constructed domain and its general form.Experimental results show that the template constraint matrix abstract domain based on rigorous linear progrmming can improve analysis performance within the allowable range of accuracy error.