Please use this identifier to cite or link to this item: https://doi.org/10.1007/978-3-642-29860-8_32
Title: Unbounded symbolic execution for program verification
Authors: Jaffar, J. 
Navas, J.A.
Santosa, A.E.
Issue Date: 2012
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)
URI: http://scholarbank.nus.edu.sg/handle/10635/41106
ISBN: 9783642298592
ISSN: 03029743
DOI: 10.1007/978-3-642-29860-8_32
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

SCOPUSTM   
Citations

20
checked on Dec 13, 2017

Page view(s)

76
checked on Dec 9, 2017

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.