In this talk, I will try to make a case for the use of data flow graphs as a suitable notion for abstractions of concurrent programs for the purpose of verification. I will talk about two successful experiences that we have had with these graphs. One is the development of an abstract interpretation framework that constructs annotated data flow graph where the annotations can come from any abstract domain such as intervals or octagons. We demonstrate how by separating the concerns of reasoning about data (computing the data invariants) and control (computing a precise enough pattern of interference among threads), we can achieve both scalability and precision for the problem of thread-state verification of concurrent programs. Moreover, we employ parameterization as an abstraction and therefore, this technique works for programs with unbounded number of threads. Duet, the tool developed based on this framework successfully verifies a variety of program assertions (memory safety, etc) for a class of linux device drivers comparing very favourably against existing tools.
In the second part of the talk, I will talk about a variation of these graphs called "Inductive Data Flow Graphs" that are the basis of a new proof technique for proving partial correctness of concurrent programs (with respect to pre/post-conditions). I will argue how inductive data flow graphs can be viewed as "concise" proof arguments for the correctness of concurrent programs, and present a sound and complete algorithmic framework for computing such proofs. This is a fundamentally new proof technique compared to classical methods such as Owicki-Gries and Rely-Guarantee.
My talk will be based on the content of the following two papers: