SPLASH 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
Wed 20 Oct 2021 15:40 - 15:55 at Zurich G - OOPSLA 2020 Papers 3 Chair(s): Anders Miltner

There is growing interest in termination reasoning for non-linear programs and, meanwhile, recent dynamic strategies have shown they are able to infer invariants for such challenging programs. These advances led us to hypothesize that perhaps such dynamic strategies for non-linear invariants could be adapted to learn recurrent sets (for non-termination) and/or ranking functions (for termination).

In this paper, we exploit dynamic analysis and draw termination and non-termination as well as static and dynamic strategies closer together in order to tackle non-linear programs. For termination, our algorithm infers ranking functions from concrete transitive closures, and, for non-termination, the algorithm iteratively collects executions and dynamically learns conditions to refine recurrent sets. Finally, we describe an integrated algorithm that allows these algorithms to mutually inform each other, taking counterexamples from a failed validation in one endeavor and crossing both the static/dynamic and term./non-term.~ lines, to create new execution samples for the other one.

We have implemented these algorithms in a new tool called DynamiTe. For non-linear programs, there are currently no SV-COMP termination benchmarks so we created new sets of 37 terminating and 37 non-terminating programs. Our empirical evaluation shows that we can effectively guess (and sometimes even validate) ranking functions and recurrent sets for programs with non-linear behaviors. Furthermore, we show that counterexamples from one failed validation can be used to generate executions for a dynamic analysis of the opposite property. Although we are focused on non-linear programs, as a point of comparison, we compare DynamiTe’s performance on linear programs with that of the state-of-the-art tool, Ultimate. Although DynamiTe is an order of magnitude slower it is nonetheless somewhat competitive and sometimes finds ranking functions where Ultimate was unable to. Ultimate cannot, however, handle the non-linear programs in our new benchmark suite.

Wed 20 Oct

Displayed time zone: Central Time (US & Canada) change

15:40 - 17:00
OOPSLA 2020 Papers 3SIGPLAN Papers at Zurich G
Chair(s): Anders Miltner The University of Texas at Austin, Texas, USA
15:40
15m
Talk
DynamiTe: Dynamic Termination and Non-termination Proofs
SIGPLAN Papers
Ton Chanh Le Stevens Institute of Technology, Timos Antonopoulos Yale University, Parisa Fathololumi Stevens Institute of Technology, Eric Koskinen Stevens Institute of Technology, ThanhVu Nguyen George Mason University
15:55
15m
Talk
TacTok: Semantics-Aware Proof Synthesis
SIGPLAN Papers
Emily First University of Massachusetts at Amherst, Yuriy Brun University of Massachusetts Amherst, Arjun Guha Northeastern University
Link to publication DOI Pre-print
16:10
15m
Talk
Towards A Unified Proof Framework for Automated Fixpoint Reasoning Using Matching Logic
SIGPLAN Papers
Xiaohong Chen University of Illinois at Urbana-Champaign, Minh-Thai Trinh Advanced Digital Sciences Center, Nishant Rodrigues University of Illinois at Urbana-Champaign, Lucas Peña University of Illinois at Urbana-Champaign, Grigore Roşu University of Illinois at Urbana-Champaign
16:25
15m
Talk
Verifying and Improving Halide’s Term Rewriting System with Program Synthesis
SIGPLAN Papers
Julie L. Newcomb University of Washington, Andrew Adams Adobe, Steven Johnson Google, Rastislav Bodik University of Washington, Shoaib Kamil Adobe Research
16:40
20m
Live Q&A
Discussion, Questions and Answers
SIGPLAN Papers