PRECISE Seminar: Data Flow Graphs for Verification of Concurrent Programs

PRECISE Seminar: Data Flow Graphs for Verification of Concurrent Programs
Thu, October 25, 2012 @ 11:30am EDT
Levine Hall - Room 512
3330 Walnut Street
Philadelphia, PA 19104
Speaker
Azadeh Farzan, Ph.D.
University of Toronto
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:

  1. Azadeh Farza, Zachary Kincaid: Verification of parameterized concurrent programs by modular reasoning about data and control. POPL 2012: 297-308.
  2. Azadeh Farza, Zachary Kincaid, and Andreas Podelski: Inductive Data Flow Graphs. To appear in POPL 2013.
Speaker Bio

Azadeh Farzan has been an Assistant Professor in the Computer Science department of University of Toronto since September 2008. She received her PhD degree from University of Illinois at Urbana-Champaign in May 2007. She was consequently a post doctoral fellow in Carnegie Mellon University before starting her current position. For more information visit www.cs.toronto.edu/~azadeh