Please use this identifier to cite or link to this item: http://scholarbank.nus.edu.sg/handle/10635/135847
Title: REASONING OVER STRINGS AND OTHER UNBOUNDED DATA STRUCTURES
Authors: TRINH MINH THAI
Keywords: Recursive Data Structures, String Solving, Entailment Checking, Web security, Program Verification, Symbolic Execution
Issue Date: 19-Jan-2017
Source: TRINH MINH THAI (2017-01-19). REASONING OVER STRINGS AND OTHER UNBOUNDED DATA STRUCTURES. ScholarBank@NUS Repository.
Abstract: Data structures play a central role in software development. While developing proper data structures is not easy, reasoning about them is even harder. The difficulty comes from their typical characteristic: the unboundedness of the data structures and/or the loops manipulating them. This makes two following fundamental issues more severe: inter-dependence between structures and data values, and complicated interactions between different data structures. In this thesis, we consider the problem of reasoning about unbounded data structures such as strings, linked lists, trees. Specifically, we propose systematic techniques for the satisfiability problem of string constraints, and the entailment proving problem for heap-allocated data structures. These two problems are of great interest: for example, while the former is important for security analysis of web applications, the latter is important for automated verification of imperative programs.
URI: http://scholarbank.nus.edu.sg/handle/10635/135847
Appears in Collections:Ph.D Theses (Open)

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

OPEN

NoneView/Download

Page view(s)

40
checked on Jan 20, 2018

Download(s)

48
checked on Jan 20, 2018

Google ScholarTM

Check


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