Please use this identifier to cite or link to this item:
Title: Symbolic Execution for Advanced Program Reasoning
Keywords: Symbolic Execution, Interpolation, Program Analysis, Verification, Testing, Debugging
Issue Date: 2-Jun-2014
Citation: VIJAYARAGHAVAN MURALI (2014-06-02). Symbolic Execution for Advanced Program Reasoning. ScholarBank@NUS Repository.
Abstract: This thesis addresses a number of program reasoning problems faced by programmers, using symbolic execution. Symbolic execution has the advantage of avoiding "infeasible" paths in the program (paths that cannot be exercised for any input), exploring which could provide spurious information about the program, misleading the programmer. However, as symbolic execution considers the feasibility of individual paths, the number of which could be exponential in general, it suffers from path explosion. To tackle this, we use the technique of "interpolation". We make significant contributions to the areas of program slicing, verification, concolic testing and trace comprehension. Our breakthroughs in program slicing include formulating the most precise slicing algorithm and the novel notion of "tree slicing". We also bring, for the first time, exponential benefits of interpolation to concolic testing, improve the performance of interpolation-based verifiers, and make strides in the understanding of execution traces using interpolants and loop invariant discovery.
Appears in Collections:Ph.D Theses (Open)

Show full item record
Files in This Item:
File Description SizeFormatAccess SettingsVersion 
thesis.pdf1.68 MBAdobe PDF



Page view(s)

checked on Oct 12, 2018


checked on Oct 12, 2018

Google ScholarTM


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