Please use this identifier to cite or link to this item:
|Title:||Unbounded symbolic execution for program verification|
|Authors:||Jaffar, J. |
|Source:||Jaffar, J.,Navas, J.A.,Santosa, A.E. (2012). Unbounded symbolic execution for program verification. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 7186 LNCS : 396-411. ScholarBank@NUS Repository. https://doi.org/10.1007/978-3-642-29860-8_32|
|Abstract:||Symbolic execution with interpolation is emerging as an alternative to cegar for software verification. The performance of both methods relies critically on interpolation in order to obtain the most general abstraction of the current symbolic or abstract state which can be shown to remain error-free. cegar naturally handles unbounded loops because it is based on abstract interpretation. In contrast, symbolic execution requires a special extension for such loops. In this paper, we present such an extension. Its main characteristic is that it performs eager subsumption, that is, it always attempts to perform abstraction in order to avoid exploring redundant symbolic states. It balances this primary desire for more abstraction with the secondary desire to maintain the strongest loop invariant, for earlier detection of infeasible paths, which entails less abstraction. Occasionally certain abstractions are not permitted because of the reachability of error states; this is the underlying mechanism which then causes selective unrolling, that is, the unrolling of a loop along relevant paths only. © 2012 Springer-Verlag.|
|Source Title:||Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|
|Appears in Collections:||Staff Publications|
Show full item record
Files in This Item:
There are no files associated with this item.
checked on Dec 13, 2017
checked on Dec 9, 2017
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.