Sound Sequentialization for Concurrent Program Verification
Fri 17 Jun 2022 02:30 - 02:50 at Kon-Tiki - Concurrency
We present a systematic investigation and experimental evaluation of a large space of algorithms for the verification of concurrent programs. The algorithms are based on sequentialization. In the analysis of concurrent programs, the general idea of sequentialization is to select a subset of interleavings, represent this subset as a sequential program, and apply a generic analysis for sequential programs. For the purpose of verification, the sequentialization has to be sound. We use the concept of a preference order to parametrize the selection, and thereby the algorithm based on sequentialization. The parametrization allows us to evaluate the impact of the preference order on the performance of the algorithm. Our experiments indicate the practical potential of sound sequentialization for concurrent program verification.
| Slides (presentation.pdf) | 754KiB |
Thu 16 JunDisplayed time zone: Pacific Time (US & Canada) change
13:30 - 14:50 | |||
13:30 20mTalk | A Flexible Type System for Fearless Concurrency PLDI Mae Milano University of California, Berkeley, Joshua Turcotti University of California, Berkeley, Andrew Myers Cornell University DOI | ||
13:50 20mTalk | A Study of Real-world Data Races in Golang PLDI DOI | ||
14:10 20mTalk | Checking Robustness to Weak Persistency Models PLDI Hamed Gorjiara University of California, Irvine, Weiyu Luo University of California, Irvine, Alex Lee University of California, Irvine, Guoqing Harry Xu University of California at Los Angeles, Brian Demsky University of California, Irvine DOI | ||
14:30 20mTalk | Sound Sequentialization for Concurrent Program Verification PLDI Azadeh Farzan University of Toronto, Dominik Klumpp University of Freiburg, Andreas Podelski University of Freiburg, Germany DOI File Attached | ||
Fri 17 JunDisplayed time zone: Pacific Time (US & Canada) change
01:30 - 02:50 | |||
01:30 20mTalk | A Flexible Type System for Fearless Concurrency PLDI Mae Milano University of California, Berkeley, Joshua Turcotti University of California, Berkeley, Andrew Myers Cornell University DOI | ||
01:50 20mTalk | A Study of Real-world Data Races in Golang PLDI DOI | ||
02:10 20mTalk | Checking Robustness to Weak Persistency Models PLDI Hamed Gorjiara University of California, Irvine, Weiyu Luo University of California, Irvine, Alex Lee University of California, Irvine, Guoqing Harry Xu University of California at Los Angeles, Brian Demsky University of California, Irvine DOI | ||
02:30 20mTalk | Sound Sequentialization for Concurrent Program Verification PLDI Azadeh Farzan University of Toronto, Dominik Klumpp University of Freiburg, Andreas Podelski University of Freiburg, Germany DOI File Attached | ||