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): Marieke Huisman, Michael Coblenz
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 Nov Times are displayed in time zone: Central Time (US & Canada) change
Thu 19 Nov
Times are displayed in time zone: Central Time (US & Canada) change
11:00 - 12:20: R-3OOPSLA at SPLASH-I +12h Chair(s): Marieke HuismanUniversity of Twente, Michael CoblenzUniversity of Maryland at College Park | |||
11:00 - 11:20 Talk | Compiling Symbolic Execution with Staging and Algebraic Effects OOPSLA Guannan WeiPurdue University, Oliver BračevacPurdue University, Shangyin TanPurdue University, Tiark RompfPurdue University Link to publication DOI Pre-print Media Attached | ||
11:20 - 11:40 Talk | Projection-Based Runtime Assertions for Testing and Debugging Quantum Programs OOPSLA Gushu LiUniversity of California at Santa Barbara, Li ZhouMax Planck Institute for Security and Privacy, Nengkun YuUniversity of Technology Sydney, Yufei DingUniversity of California at Santa Barbara, Mingsheng YingUniversity of Technology Sydney / Institute of Software at Chinese Academy of Sciences / Tsinghua University, Yuan XieUniversity of California at Santa Barbara Link to publication DOI Pre-print Media Attached | ||
11:40 - 12:00 Talk | Satune: Synthesizing Efficient SAT Encoders OOPSLA Hamed GorjiaraUniversity of California at Irvine, Guoqing Harry XuUniversity of California at Los Angeles, Brian DemskyUniversity of California at Irvine Link to publication DOI Media Attached | ||
12:00 - 12:20 Talk | The Anchor Verifier for Blocking and Non-blocking Concurrent Software OOPSLA Link to publication DOI Media Attached |
23:00 - 00:20: R-3OOPSLA at SPLASH-I Chair(s): Pranav KantUniversity of Utah, Xiangzhe XuNanjing University | |||
23:00 - 23:20 Talk | Compiling Symbolic Execution with Staging and Algebraic Effects OOPSLA Guannan WeiPurdue University, Oliver BračevacPurdue University, Shangyin TanPurdue University, Tiark RompfPurdue University Link to publication DOI Pre-print Media Attached | ||
23:20 - 23:40 Talk | Projection-Based Runtime Assertions for Testing and Debugging Quantum Programs OOPSLA Gushu LiUniversity of California at Santa Barbara, Li ZhouMax Planck Institute for Security and Privacy, Nengkun YuUniversity of Technology Sydney, Yufei DingUniversity of California at Santa Barbara, Mingsheng YingUniversity of Technology Sydney / Institute of Software at Chinese Academy of Sciences / Tsinghua University, Yuan XieUniversity of California at Santa Barbara Link to publication DOI Pre-print Media Attached | ||
23:40 - 00:00 Talk | Satune: Synthesizing Efficient SAT Encoders OOPSLA Hamed GorjiaraUniversity of California at Irvine, Guoqing Harry XuUniversity of California at Los Angeles, Brian DemskyUniversity of California at Irvine Link to publication DOI Media Attached | ||
00:00 - 00:20 Talk | The Anchor Verifier for Blocking and Non-blocking Concurrent Software OOPSLA Link to publication DOI Media Attached |