SPLASH 2022 (series) / V-OOPSLA / Consistency-Preserving Propagation for SMT Solving of Concurrent Program Verification
Consistency-Preserving Propagation for SMT Solving of Concurrent Program VerificationPre-recorded
The happens-before orders have been widely adopted to model thread interleaving behaviors of concurrent programs. A dedicated ordering theory solver, usually composed of theory propagation, consistency checking, and conflict clause generation, plays a central role in concurrent program verification. We propose a novel preventive reasoning approach that automatically preserves the ordering consistency and makes consistency checking and conflict clause generation omissible. We implement our approach in a prototype tool and conduct experiments on credible benchmarks; results reveal a significant improvement over existing state-of-the-art concurrent program verifiers.
Wed 30 NovDisplayed time zone: Auckland, Wellington change
Wed 30 Nov
Displayed time zone: Auckland, Wellington change
21:00 - 22:45 | Session 2V-OOPSLA at Virtual Airmeet Room Chair(s): Sophia Drossopoulou Meta and Imperial College London | ||
21:00 15mTalk | Taming Transitive Redundancy for Context-Free Language ReachabilityPre-recorded V-OOPSLA Yuxiang Lei University of Technology Sydney, Yulei Sui University of New South Wales, Sydney, Shuo Ding Georgia Institute of Technology, Qirun Zhang Georgia Institute of Technology DOI | ||
21:15 15mTalk | Scalable Linear Invariant Generation with Farkas’ Lemma V-OOPSLA Hongming Liu Shanghai Jiao Tong University, Hongfei Fu Shanghai Jiao Tong University, zhiyong yu Shanghai Jiao Tong University, Jiaxin Song Shanghai Jiao Tong University, Guoqiang Li Shanghai Jiao Tong University DOI | ||
21:30 15mTalk | Consistency-Preserving Propagation for SMT Solving of Concurrent Program VerificationPre-recorded V-OOPSLA DOI | ||
21:45 15mTalk | Oracle-Free Repair Synthesis for Floating-Point ProgramsPre-recorded V-OOPSLA Daming Zou ETH Zurich, Yuchen Gu Peking University, Yuanfeng Shi Peking University, Mingzhe Wang Princeton University, Yingfei Xiong Peking University, Zhendong Su ETH Zurich DOI | ||
22:00 15mTalk | Neurosymbolic Repair for Low-Code Formula Languages V-OOPSLA Rohan Bavishi University of California at Berkeley, Harshit Joshi Microsoft, José Pablo Cambronero Microsoft, Anna Fariha Microsoft, Sumit Gulwani Microsoft, Vu Le Microsoft, Ivan Radiček Microsoft, Ashish Tiwari Microsoft DOI | ||
22:15 30mLive Q&A | Q&A for Session 2 V-OOPSLA |