Please use this identifier to cite or link to this item:
|Title:||Path-sensitive resource analysis compliant with assertions|
|Source:||Chu, D.-H.,Jaffar, J. (2013). Path-sensitive resource analysis compliant with assertions. 2013 Proceedings of the International Conference on Embedded Software, EMSOFT 2013 : -. ScholarBank@NUS Repository. https://doi.org/10.1109/EMSOFT.2013.6658593|
|Abstract:||We consider the problem of bounding the worst-case resource usage of programs, where assertions about valid program executions may be enforced at selected program points. It is folklore that to be precise, path-sensitivity (up to loops) is needed. This entails unrolling loops in the manner of symbolic simulation. To be tractable, however, the treatment of the individual loop iterations must be greedy in the sense once analysis is finished on one iteration, we cannot backtrack to change it. We show that under these conditions, enforcing assertions produces unsound results. The fundamental reason is that complying with assertions requires the analysis to be fully sensitive (also with loops) wrt. the assertion variables. We then present an algorithm where the treatment of each loop is separated in two phases. The first phase uses a greedy strategy in unrolling the loop. This phase explores what is conceptually a symbolic execution tree, which is of enormous size, while eliminates infeasible paths and dominated paths that guaranteed not to contribute to the worst case bound. A compact representation is produced at the end of this phase. Finally, the second phase attacks the remaining problem, to determine the worst-case path in the simplified tree, excluding all paths that violate the assertions from bound calculation. Scalability, in both phases, is achieved via an adaptation of a dynamic programming algorithm. © 2013 IEEE.|
|Source Title:||2013 Proceedings of the International Conference on Embedded Software, EMSOFT 2013|
|Appears in Collections:||Staff Publications|
Show full item record
Files in This Item:
There are no files associated with this item.
checked on Mar 8, 2018
checked on Mar 10, 2018
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.