SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Tue 17 Nov 2020 17:00 - 17:20 at SPLASH - T-6B
Wed 18 Nov 2020 05:00 - 05:20 at SPLASH - T-6B

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.

Tue 17 Nov
Times are displayed in time zone: Central Time (US & Canada) change

17:00 - 18:20: T-6BOOPSLA at SPLASH +12h
17:00 - 17:20
Talk
OOPSLA
Ton Chanh LeStevens Institute of Technology, Timos AntonopoulosYale University, Parisa FathololumiStevens Institute of Technology, Eric KoskinenStevens Institute of Technology, ThanhVu NguyenUniversity of Nebraska, Lincoln
17:20 - 17:40
Talk
OOPSLA
Eric AtkinsonMIT, Michael CarbinMassachusetts Institute of Technology, USA
17:40 - 18:00
Talk
OOPSLA
Julia BelyakovaNortheastern University, USA, Benjamin ChungNortheastern University, Jack GelinasNortheastern University, Jameson NashJulia Computing, Ross TateCornell University, Jan VitekNortheastern University
18:00 - 18:20
Talk
OOPSLA
Robert GriesemerGoogle, Raymond HuUniversity of Hertfordshire, Wen KokkeUniversity of Edinburgh, Julien LangeRoyal Holloway, University of London, Ian Lance TaylorGoogle, Bernardo ToninhoUniversidade Nova de Lisboa and NOVA LINCS, Philip WadlerUniversity of Edinburgh, UK, Nobuko YoshidaImperial College London

Wed 18 Nov
Times are displayed in time zone: Central Time (US & Canada) change

05:00 - 06:20: T-6BOOPSLA at SPLASH
05:00 - 05:20
Talk
OOPSLA
Ton Chanh LeStevens Institute of Technology, Timos AntonopoulosYale University, Parisa FathololumiStevens Institute of Technology, Eric KoskinenStevens Institute of Technology, ThanhVu NguyenUniversity of Nebraska, Lincoln
05:20 - 05:40
Talk
OOPSLA
Eric AtkinsonMIT, Michael CarbinMassachusetts Institute of Technology, USA
05:40 - 06:00
Talk
OOPSLA
Julia BelyakovaNortheastern University, USA, Benjamin ChungNortheastern University, Jack GelinasNortheastern University, Jameson NashJulia Computing, Ross TateCornell University, Jan VitekNortheastern University
06:00 - 06:20
Talk
OOPSLA
Robert GriesemerGoogle, Raymond HuUniversity of Hertfordshire, Wen KokkeUniversity of Edinburgh, Julien LangeRoyal Holloway, University of London, Ian Lance TaylorGoogle, Bernardo ToninhoUniversidade Nova de Lisboa and NOVA LINCS, Philip WadlerUniversity of Edinburgh, UK, Nobuko YoshidaImperial College London