Seminars

Data Flow Graphs for Verification of Concurrent Programs PDF
Azadeh Farzan, Department of Computer Science, University of Toronto

10/24/2012, 10am, GHC 9115

Abstract

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:

Azadeh Farzan, Zachary Kincaid: Verification of parameterized concurrent programs by modular reasoning about data and control. POPL 2012: 297-308.

Azadeh Farzan, Zachary Kincaid, and Andreas Podelski: Inductive Data Flow Graphs. To appear in POPL 2013.

Biography

Azadeh Farzan is a Assistant Professor at University of Toronto and
her research focuses on Software Verification, Programming
Languages, Formal Methods, and Security (all with an emphasis on
concurrency-related issues)

http://www.cs.toronto.edu/~azadeh/index.html