Please use this identifier to cite or link to this item:
Title: Interpolation Methods for Symbolic Execution
Keywords: Symbolic Execution, Interpolation, Abstraction Learning, Program Path Analysis, Concurrent Verification, WCET
Issue Date: 3-Dec-2012
Citation: 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.
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).
We address the challenge by building custom interpolation methods, in order to effectively reduce the size of the explored tree on-the-fly.
Appears in Collections:Ph.D Theses (Open)

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



Page view(s)

checked on Apr 20, 2019


checked on Apr 20, 2019

Google ScholarTM


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