Please use this identifier to cite or link to this item: http://scholarbank.nus.edu.sg/handle/10635/80195
Title: Symbolic Execution for Advanced Program Reasoning
Authors: VIJAYARAGHAVAN MURALI
Keywords: Symbolic Execution, Interpolation, Program Analysis, Verification, Testing, Debugging
Issue Date: 2-Jun-2014
Source: 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.
URI: http://scholarbank.nus.edu.sg/handle/10635/80195
Appears in Collections:Ph.D Theses (Open)

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

OPEN

NoneView/Download

Page view(s)

139
checked on Feb 16, 2018

Download(s)

249
checked on Feb 16, 2018

Google ScholarTM

Check


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