Loop Summarization and Termination Analysis

Publication Type:

Conference Paper

Authors:

Tsitovich, A.; Sharygina, N.; Wintersteiger, C.M.; Kroening, D.

Source:

International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Springer, Volume 6605, Saarbr├╝cken, Germany, p.81-95 (2011)

Abstract:

We present a technique for program termination analysis based on loop summarization. The algorithm relies on a library of abstract domains to discover well-founded transition invariants. In contrast to state-of-the-art methods it aims to construct a complete ranking argument for all paths through a loop at once, thus avoiding expensive enumeration of individual paths. Compositionality is used as a completeness criterion for the discovered transition invariants. The practical efficiency of the approach is evaluated using a set of Windows device drivers.

@inproceedings { twks11,
	title = {Loop Summarization and Termination Analysis},
	booktitle = {International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
	volume = {6605},
	year = {2011},
	pages = {81-95},
	publisher = {Springer},
	organization = {Springer},
	address = {Saarbr├╝cken, Germany},
	URL = {http://dx.doi.org/10.1007/978-3-642-19835-9_9},
	author = {Aliaksei Tsitovich and  Natasha Sharygina and  Christoph M. Wintersteiger and  Kroening, Daniel}
}

AttachmentSize
tswk11.pdf337.7 KB