Duet: static analysis for unbounded concurrency

About

Duet¹ is a static analysis tool designed for analyzing concurrent programs, where the number of threads cannot be statically bounded. It accomplishes this task by decomposing the analysis problem into two components – one that analyzes data, and one that analyzes control. These two components interact with eachother to compute a sound overapproximation of the dynamic behaviours of a program.

People

Azadeh Farzan

Zachary Kincaid

Download

Duet is not yet ready for general release. However, we plan to make source and binary distributions available soon.

Experiments

Experiments for [FK12] will be available soon.

Publications

[FK12]	Azadeh Farzan and Zachary Kincaid. Verification of parameterized concurrent programs by modular reasoning about data and control. In Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL '12, pages 297-308, New York, NY, USA, 2012. ACM. [ abstract \| bib \| DOI ]
[FK10]	Azadeh Farzan and Zachary Kincaid. Compositional bitvector analysis for concurrent programs with nested locks. In SAS, pages 253-270, 2010. [ abstract \| bib ]

Related work

Tools for model checking parameterized Boolean programs

Boom (implements dynamic cutoff detection)
Getafix (implements linear interfaces)

Footnotes:

¹ This work is partially supported by a National Science and Engineering Research Council (NSERC) Discovery Grant