SPLASH 2020 (series) / OOPSLA /
The Anchor Verifier for Blocking and Non-blocking Concurrent Software
Thu 19 Nov 2020 12:00 - 12:20 at SPLASH-I - R-3 Chair(s): Michael Coblenz, Marieke Huisman
Fri 20 Nov 2020 00:00 - 00:20 at SPLASH-I - R-3 Chair(s): Pranav Kant, Xiangzhe Xu
Fri 20 Nov 2020 00:00 - 00:20 at SPLASH-I - R-3 Chair(s): Pranav Kant, Xiangzhe Xu
Verifying the correctness of concurrent software with subtle
synchronization is notoriously challenging. We present the
Anchor verifier, which is based on a new formalism for
specifying synchronization disciplines that describes both (1)
what memory accesses are permitted, and (2) how each permitted
access commutes with concurrent operations of other threads (to
facilitate reduction proofs). Anchor supports the verification
of both lock-based blocking and cas-based non-blocking
algorithms. Experiments on a variety concurrent data structures
and algorithms show that Anchor significantly reduces the burden
of concurrent verification.
Thu 19 NovDisplayed time zone: Central Time (US & Canada) change
Thu 19 Nov
Displayed time zone: Central Time (US & Canada) change
11:00 - 12:20 | R-3OOPSLA at SPLASH-I +12h Chair(s): Michael Coblenz University of Maryland at College Park, Marieke Huisman University of Twente | ||
11:00 20mTalk | Compiling Symbolic Execution with Staging and Algebraic Effects OOPSLA Guannan Wei Purdue University, Oliver Bračevac Purdue University, Shangyin Tan Purdue University, Tiark Rompf Purdue University Link to publication DOI Pre-print Media Attached | ||
11:20 20mTalk | Projection-Based Runtime Assertions for Testing and Debugging Quantum Programs OOPSLA Gushu Li University of California at Santa Barbara, Li Zhou Max Planck Institute for Security and Privacy, Nengkun Yu University of Technology Sydney, Yufei Ding University of California at Santa Barbara, Mingsheng Ying University of Technology Sydney / Institute of Software at Chinese Academy of Sciences / Tsinghua University, Yuan Xie University of California at Santa Barbara Link to publication DOI Pre-print Media Attached | ||
11:40 20mTalk | Satune: Synthesizing Efficient SAT Encoders OOPSLA Hamed Gorjiara University of California at Irvine, Guoqing Harry Xu University of California at Los Angeles, Brian Demsky University of California at Irvine Link to publication DOI Media Attached | ||
12:00 20mTalk | The Anchor Verifier for Blocking and Non-blocking Concurrent Software OOPSLA Link to publication DOI Media Attached | ||
23:00 - 00:20 | |||
23:00 20mTalk | Compiling Symbolic Execution with Staging and Algebraic Effects OOPSLA Guannan Wei Purdue University, Oliver Bračevac Purdue University, Shangyin Tan Purdue University, Tiark Rompf Purdue University Link to publication DOI Pre-print Media Attached | ||
23:20 20mTalk | Projection-Based Runtime Assertions for Testing and Debugging Quantum Programs OOPSLA Gushu Li University of California at Santa Barbara, Li Zhou Max Planck Institute for Security and Privacy, Nengkun Yu University of Technology Sydney, Yufei Ding University of California at Santa Barbara, Mingsheng Ying University of Technology Sydney / Institute of Software at Chinese Academy of Sciences / Tsinghua University, Yuan Xie University of California at Santa Barbara Link to publication DOI Pre-print Media Attached | ||
23:40 20mTalk | Satune: Synthesizing Efficient SAT Encoders OOPSLA Hamed Gorjiara University of California at Irvine, Guoqing Harry Xu University of California at Los Angeles, Brian Demsky University of California at Irvine Link to publication DOI Media Attached | ||
00:00 20mTalk | The Anchor Verifier for Blocking and Non-blocking Concurrent Software OOPSLA Link to publication DOI Media Attached | ||