Abstract:

Static program analysis with abstract interpretation has been successfully applied to industry in order to avoid runtime errors and ensure the correctness of the software. Abstract domain is one of the important aspects in abstract interpretation theory. However, most of the existing numerical abstract domains cannot express non-convex properties. These limitations often affect the precision of numerical analysis and even lead to more false alarms.We propose a numerical abstract domain based on two-interval octagonal constraints. This abstract domain allows us to represent invariants of the form x±y∈［a,b］∪［c,d］, where x  and y are variable values and a,b,c,d∈R. Domain elements in this abstract domain are represented by two-interval octagonal constraints, so the new abstract domain can express certain non-convex properties and is more expressive than the octagon abstract domain, with only a small overhead in the computational complexity of domain operation.

Key words: abstract interpretation, octagon abstract domain, two-interval, transfer function