Technical Perspactive Abstracting Abstract Machines

摘要

The goal of program analysis is to stati cally predict runtime properties of pro grams without running them. The se mantic approach to program analysis originates in Cousot's path-breaking work on abstract interpretation: start from a formal mathematical model of program execution-a semantics-and approximate it with Galois connec tions (or similar means) into a com putable model based on lattices of runtime properties that accounts for all possible execution paths. Each pro gram gives rise to a collection of equa tions that are then typically solved by fixed-point iteration.