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. © 2011 Springer-Verlag.
Cite
CITATION STYLE
Tsitovich, A., Sharygina, N., Wintersteiger, C. M., & Kroening, D. (2011). Loop summarization and termination analysis. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6605 LNCS, pp. 81–95). Springer Verlag. https://doi.org/10.1007/978-3-642-19835-9_9
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
