Program Analysis as Model Checking of Abstract Interpretations

摘要: This paper presents a collection of techniques, methodology, in which abstract interpretation, flow analysis, and model checking are employed the representation, abstraction, analysis programs. The methodology shows areas intersection different techniques as well opportunites that exist when one technique is used support another. presented three-step process: First, from (small-step) operational semantics definition program, constructs program model, state-transition system encodes program’s executions. Second, abstraction upon performed, reducing detail information model’s nodes arcs. Finally, analyzed for properties its states paths.