Personal tools
You are here: Home Events Abstract Archives 1997 Using Model Checking to Understand the Relationship between Abstract Interpretation and Data Flow Analysis

Using Model Checking to Understand the Relationship between Abstract Interpretation and Data Flow Analysis

David Schmidt (Kansas State University, USA) LFCS Theory Seminar Room 2511, JCMB, King's Buildings 3.30pm, Monday 7th April 1997

Although data flow analysis ("DFA") is as old as the hills, and abstract interpretation ("AI") has reached its 20th birthday, the precise relationship between the classic, flowchart-based DFA algorithms (e.g., available expressions, reaching definitions, live variables, very busy expressions) and the AI of flowcharts has never been simply stated. (In Cousot&Cousot77, available expressions was called a "syntactic analysis" and placed outside of the realm of "semantically based" AI.)

This talk attempts to use concepts from model checking to explain the exact relationship between the classic DFAs and AI: First, a flowchart's AI is classified as being either a safe or a live simulation of the flowchart's concrete interpretation. Next, the AI's collecting semantics is classified as being either state- or path-based. Finally, the mu-calculus is introduced as a language for defining path-based collecting semantics.

The classic DFAs are recoded mechanically as formulas in the mu-calculus, and a DFA is claimed to be merely a model check of a flowchart's AI. Unfortunately, two of the classic DFAs mentioned above are unsound with respect to the AIs they are meant to model check, which might explain some of the confusion regarding the relation of DFAs to AI. The unsoundness is repaired (or at least, explained), and the talk concludes with idle speculation regarding the importance of model checking to the futures of DFA and AI.

Document Actions