CORE: Foundations of Practical Concurrency Analysis

With the proliferation of concurrent programming, it is increasingly important to develop practical tools for concurrency analysis. The CORE project is an ongoing investigation of the foundations of concurrency analysis for modern software.
Today's programs typically use libraries that implement highly concurrent data structures and hide much of the underlying complexity. A primary goal of CORE is to enable analysis of the usage of such data structures. This requires a shift from reasoning about low-level memory access to reasoning about high-level data structure interfaces. Another vital aspect of program analysis is scaling to realistic programs. A key tool in designing scalable algorithms is exploiting the structure of the problem at hand. That is why, CORE aims to understand the interplay between analysis complexity and the concurrency structure present in many programs.

Publications

Serializability for Eventual Consistency: Criterion, Analysis, and Applications
Lucas Brutschy, Dimitar Dimitrov, Peter Müller, Martin Vechev
ACM POPL 2017
PDF
Learning Commutativity Specifications
Timon Gehr, Dimitar Dimitrov, Martin Vechev
CAV 2015
PDF Specs: PDF Source: ZIP
Race Detection in Two Dimensions
Dimitar Dimitrov, Martin Vechev, Vivek Sarkar
ACM SPAA 2015
PDF
Commutativity Race Detection
Dimitar Dimitrov, Veselin Raychev, Martin Vechev, Eric Koskinen
ACM PLDI 2014
PDF