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

Invariant generation is a classical problem to automatically generate invariants to aid the formal analysis of programs. In this work, we consider the problem of generating tight linear-invariants over affine programs (i.e., programs with affine guards and updates)
without a prescribed goal property.
In the literature, the only known sound and complete characterization to solve this problem is via Farkas' Lemma (FL), and has been
implemented through either quantifier elimination or reasonable heuristics.
Although FL-based approaches can generate highly accurate linear invariants from the completeness of FL, the main bottleneck to applying these approaches is the scalability issue caused by either non-linear constraints or combinatorial explosion.
We base our approach on the only practical FL-based approach [Sankaranarayanan~\emph{et al.}, SAS 2004] that applies FL with reasonable heuristics, and develop two novel and independent improvements to leverage the scalability. The first improvement is the novel idea to generate invariants at one program location in a single invariant-generation process, so that the invariants for each location are generated separately rather than together in a single computation. This idea naturally leads to a parallel processing that divides the invariant-generation task for all program locations by assigning the locations separately to multiple processors. Moreover, the idea enables us to develop detailed technical improvements to further reduce the combinatorial explosion in the original work [Sankaranarayanan~\emph{et al.}, SAS 2004].
The second improvement is a segmented subsumption testing in the CNF-to-DNF expansion that allows discovering more local subsumptions in advance.
We formally prove that our approach has the same accuracy as the original work and thus does not incur accuracy loss on the generated invariants.
Moreover, experimental results on representative benchmarks involving non-trivial linear invariants demonstrate that our approach improves the runtime of the original work by several orders of magnitude, even in the non-parallel scenario that sums up the execution time for all program locations.
Hence, our approach constitutes the first significant improvement in FL-based approaches for linear invariant generation after almost two decades.

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 Technology 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