Loopster: Static loop termination analysis

Xiaofei Xie, Bihuan Chen, Liang Zou, Shang Wei Lin, Yang Liu, Xiaohong Li

研究成果: Chapter in Book/Report/Conference proceedingConference contribution

3 被引用数 (Scopus)

抄録

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×+ performance improvement compared to the state-of-the-art tools.

本文言語英語
ホスト出版物のタイトルESEC/FSE 2017 - Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering
編集者Andrea Zisman, Eric Bodden, Wilhelm Schafer, Arie van Deursen
出版社Association for Computing Machinery
ページ84-94
ページ数11
ISBN(電子版)9781450351058
DOI
出版ステータス出版済み - 8 21 2017
外部発表はい
イベント11th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE 2017 - Paderborn, ドイツ
継続期間: 9 4 20179 8 2017

出版物シリーズ

名前Proceedings of the ACM SIGSOFT Symposium on the Foundations of Software Engineering
Part F130154

会議

会議11th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE 2017
国/地域ドイツ
CityPaderborn
Period9/4/179/8/17

All Science Journal Classification (ASJC) codes

  • ソフトウェア

フィンガープリント

「Loopster: Static loop termination analysis」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル