Please use this identifier to cite or link to this item: http://scholarbank.nus.edu.sg/handle/10635/37900
Title: Interpolation Methods for Symbolic Execution
Authors: CHU DUC HIEP
Keywords: Symbolic Execution, Interpolation, Abstraction Learning, Program Path Analysis, Concurrent Verification, WCET
Issue Date: 3-Dec-2012
Source: CHU DUC HIEP (2012-12-03). Interpolation Methods for Symbolic Execution. ScholarBank@NUS Repository.
Abstract: Symbolic execution is an approach for program reasoning that uses symbolic values as inputs instead of actual data, and it represents the values of program variables as symbolic expressions of the input symbolic values. Symbolic execution was first developed for program testing, but it has been subsequently used for test case and verification condition generation, among others. <br> This thesis applies symbolic execution to two important and extremely hard application areas, namely program path analysis for worst-case resource usage and safety verification of concurrent systems. The foremost challenge for symbolic execution is the exponential number of symbolic paths. This challenge is further aggravated due to the existence of loops (in program path analysis) and interleavings (in safety verification of concurrent systems). <br> We address the challenge by building custom interpolation methods, in order to effectively reduce the size of the explored tree on-the-fly.
URI: http://scholarbank.nus.edu.sg/handle/10635/37900
Appears in Collections:Ph.D Theses (Open)

Show full item record
Files in This Item:
File Description SizeFormatAccess SettingsVersion 
ChuDH.pdf2.01 MBAdobe PDF

OPEN

NoneView/Download

Page view(s)

224
checked on Dec 11, 2017

Download(s)

191
checked on Dec 11, 2017

Google ScholarTM

Check


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