Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

9-2017

Abstract

Loop termination is an important problem for proving the correctness of a system and ensuring that the system always reacts. Existing loop termination analysis techniques mainly depend on the synthesis of ranking functions, which is often expensive. In this paper, we present a novel approach, named Loopster, which performs an efficient static analysis to decide the termination for loops based on path termination analysis and path dependency reasoning. Loopster adopts a divide-and-conquer approach: (1) we extract individual paths from a target multi-path loop and analyze the termination of each path, (2) analyze the dependencies between each two paths, and then (3) determine the overall termination of the target loop based on the relations among paths. We evaluate Loopster by applying it on the loop termination competition benchmark and three real-world projects. The results show that Loopster is effective in a majority of loops with better accuracy and 20 \texttimes{}+ performance improvement compared to the state-of-the-art tools.

Keywords

Loop Termination, Reachability, Path Dependency Automaton

Discipline

Programming Languages and Compilers | Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, Paderborn, Germany, September 4-8

First Page

84

Last Page

94

ISBN

9781450351058

Identifier

10.1145/3106237.3106260

Publisher

Association for Computing Machinery

City or Country

Paderborn, Germany

Download

Share

COinS