School of Computing

Loop Leaping with Closures

Sebastian Biallas, J"org Brauer, Andy King, and Stefan Kowalewski

In Antoine Min'e and David A. Schmidt, editors, Nineteenth Static Analysis Symposium, volume 7460 of Lecture Notes in Computer Science, pages 214-230. Springer, September 2012 ARCoSS subline.

Abstract

Loop leaping is the colloquial name given to a form of program analysis in which summaries are derived for nested loops starting from the innermost loop and proceeding in a bottom-up fashion considering one more loop at a time. Loop leaping contrasts with classical approaches to finding loop invariants that are iterative; loop leaping is compositional requiring each stratum in the nest of loops to be considered exactly once. The approach is attractive in predicate abstraction where disjunctive domains are increasingly used that present long ascending chains. This paper proposes a simple and an efficient approach for loop leaping for these domains based on viewing loops as closure operators.

Download publication 235 kbytes (PDF)

Bibtex Record

@inproceedings{3230,
author = {Sebastian Biallas and J"{o}rg Brauer and Andy King and Stefan Kowalewski},
title = {Loop {L}eaping with {C}losures},
month = {September},
year = {2012},
pages = {214-230},
keywords = {abstract interpretation, predicate abstraction, bottom-up, compositional analysis},
note = {ARCoSS subline},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2012/3230},
    publication_type = {inproceedings},
    submission_id = {2028_1340019206},
    booktitle = {Nineteenth Static Analysis Symposium},
    editor = {Antoine Min'e and David A. Schmidt},
    volume = {7460},
    series = {Lecture Notes in Computer Science},
    publisher = {Springer},
    refereed = {yes},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 24/07/2012 16:36