LFCS Theory Seminar
Room 2511, JCMB, King's Buildings
3.30pm, Monday 7th April 1997

*NOTE NONSTANDARD DAY AND TIME*

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

Speaker: David Schmidt (Kansas State University, USA)

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.