Abstract Interpretation and Finite Domain Symbolic Constraints

摘要: Abstract interpretation is a general methodology for building static analyses which are useful program optimization and verification. Finite domain symbolic constraints constitute restricted class of first order formulas enjoy efficient representations. In this paper, it shown how finite can be used to implement whole abstract domains applicable any programming paradigm. Some interesting accuracy properties these discussed. The approach further developed in the context logic related well-known Prop showing that combining with bottom-up provides at same time accurate, specializable. (Such called on-line, goal-independent or condensing.)