SPLASH 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand
Wed 30 Nov 2022 21:45 - 22:00 at Virtual Airmeet Room - Session 2 Chair(s): Sophia Drossopoulou

The floating-point representation provides widely-used data types (such as float and double) for modern numerical software. Numerical errors are inherent due to floating-point’s approximate nature, and pose an important, well-known challenge. It is nontrivial to fix/repair numerical code to reduce numerical errors — it requires either numerical expertise (for manual fixing) or high-precision oracles (for automatic repair); both are difficult requirements. To tackle this challenge, this paper introduces a principled dynamic approach that is fully automated and oracle-free for effectively repairing floating-point errors. The key of our approach is the novel notion of micro-structure that characterizes structural patterns of floating-point errors. We leverage micro-structures’ statistical information on floating-point errors to effectively guide repair synthesis and validation. Compared with existing state-of-the-art repair approaches, our work is fully automatic and has the distinctive benefit of not relying on the difficult to obtain high-precision oracles. Evaluation results on 36 commonly-used numerical programs show that our approach is highly efficient and effective: (1) it is able to synthesize repairs instantaneously, and (2) versus the original programs, the repaired programs have orders of magnitude smaller floating-point errors, while having faster runtime performance.

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
15m
Talk
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
15m
Talk
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
15m
Talk
Consistency-Preserving Propagation for SMT Solving of Concurrent Program VerificationPre-recorded
V-OOPSLA
Zhihang Sun Tsinghua University, Hongyu Fan Tsinghua University, Fei He Tsinghua University
DOI
21:45
15m
Talk
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
15m
Talk
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
30m
Live Q&A
Q&A for Session 2
V-OOPSLA