SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Tue 17 Nov 2020 17:00 - 17:20 at SPLASH-III - T-6B Chair(s): Todd Millstein, Manu Sridharan
Wed 18 Nov 2020 05:00 - 05:20 at SPLASH-III - T-6B Chair(s): Sorav Bansal, Olivier Fl├╝ckiger

There is growing interest in termination reasoning for nonlinear 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 nonlinear 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 nonlinear 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 termination/non-termination lines, to create new execution samples for the other one.

We have implemented these algorithms in a new tool called DynamiTe. For nonlinear programs, there are currently no SV-COMP termination benchmarks so we created new sets of 38 terminating and 39 non-terminating programs. Our empirical evaluation shows that we can effectively guess (and sometimes even validate) ranking functions and recurrent sets for programs with nonlinear 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 nonlinear 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 nonlinear programs in our new benchmark suite.

Tue 17 Nov

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

17:00 - 18:20
T-6BOOPSLA at SPLASH-III +12h
Chair(s): Todd Millstein University of California at Los Angeles, Manu Sridharan University of California at Riverside
17:00
20m
Talk
DynamiTe: Dynamic Termination and Non-termination Proofs
OOPSLA
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 University of Nebraska-Lincoln
Link to publication DOI Media Attached
17:20
20m
Talk
Programming and Reasoning with Partial Observability
OOPSLA
Eric Atkinson Massachusetts Institute of Technology, Michael Carbin Massachusetts Institute of Technology
Link to publication DOI Media Attached
17:40
20m
Talk
World Age in Julia: Optimizing Method Dispatch in the Presence of Eval
OOPSLA
Julia Belyakova Northeastern University, Benjamin Chung Northeastern University, Jack Gelinas Northeastern University, Jameson Nash Julia Computing, Ross Tate Cornell University, Jan Vitek Northeastern University / Czech Technical University
Link to publication DOI Media Attached
18:00
20m
Talk
Featherweight Go
OOPSLA
Robert Griesemer Google, Raymond Hu University of Hertfordshire, Wen Kokke University of Edinburgh, Julien Lange Royal Holloway University of London, Ian Lance Taylor Google, Bernardo Toninho Nova University of Lisbon / NOVA-LINCS, Philip Wadler University of Edinburgh, Nobuko Yoshida Imperial College London
Link to publication DOI Media Attached

Wed 18 Nov

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

05:00 - 06:20
T-6BOOPSLA at SPLASH-III
Chair(s): Sorav Bansal IIT Delhi and CompilerAI Labs, Olivier Fl├╝ckiger Northeastern University
05:00
20m
Talk
DynamiTe: Dynamic Termination and Non-termination Proofs
OOPSLA
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 University of Nebraska-Lincoln
Link to publication DOI Media Attached
05:20
20m
Talk
Programming and Reasoning with Partial Observability
OOPSLA
Eric Atkinson Massachusetts Institute of Technology, Michael Carbin Massachusetts Institute of Technology
Link to publication DOI Media Attached
05:40
20m
Talk
World Age in Julia: Optimizing Method Dispatch in the Presence of Eval
OOPSLA
Julia Belyakova Northeastern University, Benjamin Chung Northeastern University, Jack Gelinas Northeastern University, Jameson Nash Julia Computing, Ross Tate Cornell University, Jan Vitek Northeastern University / Czech Technical University
Link to publication DOI Media Attached
06:00
20m
Talk
Featherweight Go
OOPSLA
Robert Griesemer Google, Raymond Hu University of Hertfordshire, Wen Kokke University of Edinburgh, Julien Lange Royal Holloway University of London, Ian Lance Taylor Google, Bernardo Toninho Nova University of Lisbon / NOVA-LINCS, Philip Wadler University of Edinburgh, Nobuko Yoshida Imperial College London
Link to publication DOI Media Attached