[PRL] Fwd: [MIT-PL] TALK:Friday 5-10-13 Data Flow Graphs for Verification of Concurrent Programs

[David Van Horn]

-------- Original Message --------
Subject: [MIT-PL] TALK:Friday 5-10-13 Data Flow Graphs for Verification 
of Concurrent Programs
Date: Sat, 04 May 2013 17:01:02 -0400
From: Csail Event Calendar <eventcalendar at csail.mit.edu>
To: pl at lists.csail.mit.edu


Data Flow Graphs for Verification of Concurrent Programs
Speaker: Azadeh Farzan
Speaker Affiliation: University of Toronto
Host: Armando Solar-Lezama

Date: 5-10-2013
Time: 11:00 AM - 12:00 AM
Refreshments: 10:45 AM
Location: D-463 (Star)

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 favorably
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.

Relevant URL(S):
For more information please contact: Armando Solar-Lezama, 617-258-9727, 
asolar at csail.mit.edu

_______________________________________________
Pl mailing list
Pl at lists.csail.mit.edu
https://lists.csail.mit.edu/mailman/listinfo/pl
http://projects.csail.mit.edu/pl