2016
Tighter Loop Bound Analysis
ČADEK, Pavel; Jan STREJČEK and Marek TRTÍKBasic information
Original name
Tighter Loop Bound Analysis
Authors
ČADEK, Pavel; Jan STREJČEK and Marek TRTÍK
Edition
Berlin, Heidelberg, Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, p. 512-527, 16 pp. 2016
Publisher
Springer
Other information
Language
English
Type of outcome
Proceedings paper
Field of Study
10201 Computer sciences, information science, bioinformatics
Country of publisher
Germany
Confidentiality degree
is not subject to a state or trade secret
Publication form
printed version "print"
Impact factor
Impact factor: 0.402 in 2005
Marked to be transferred to RIV
Yes
RIV identification code
RIV/00216224:14330/16:00088246
Organization unit
Faculty of Informatics
ISBN
978-3-319-46519-7
ISSN
UT WoS
EID Scopus
Keywords in English
loop bounds; symbolic execution
Tags
Tags
International impact, Reviewed
Changed: 13/5/2020 19:27, RNDr. Pavel Šmerk, Ph.D.
Abstract
In the original language
We present a new algorithm for computing upper bounds on the number of executions of each program instruction during any single program run. The upper bounds are expressed as functions of program input values. The algorithm is primarily designed to produce bounds that are relatively tight, i.e. not unnecessarily blown up. The upper bounds for instructions allow us to infer loop bounds, i.e. upper bounds on the number of loop iterations. Experimental results show that the algorithm implemented in a prototype tool Looperman often produces tighter bounds than current tools for loop bound analysis.
Links
| GBP202/12/G061, research and development project |
|