Biallas, Sebastian and Brauer, Jorg and King, Andy and Kowalewski, Stefan (2012) Loop Leaping with Closures (proof appendix for conference submission). Technical report. University of Kent, School of Computing (KAR id:37622)
PDF
Language: English |
|
Download this file (PDF/238kB) |
Preview |
Request a format suitable for use with assistive technology e.g. a screenreader | |
Official URL: http://www.cs.kent.ac.uk/pubs/2012/3230/ |
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.
Item Type: | Reports and Papers (Technical report) |
---|---|
Subjects: | A General Works |
Divisions: | Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing |
Depositing User: | Andy King |
Date Deposited: | 13 Dec 2013 15:18 UTC |
Last Modified: | 05 Nov 2024 10:21 UTC |
Resource URI: | https://kar.kent.ac.uk/id/eprint/37622 (The current URI for this page, for reference purposes) |
- Link to SensusAccess
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):