Please use this identifier to cite or link to this item: http://scholarbank.nus.edu.sg/handle/10635/13161
Title: A framework for program reasoning based on constraint traces
Authors: ANDREW EDWARD SANTOSA
Keywords: program verification, program analysis, symbolic execution, abstraction, symmetry reduction, constraint logic programming
Issue Date: 23-May-2008
Source: ANDREW EDWARD SANTOSA (2008-05-23). A framework for program reasoning based on constraint traces. ScholarBank@NUS Repository.
Abstract: We propose a CLP-based framework that accommodates both program analysis and program verification approaches. Our framework is centered on a general verification condition computation algorithm which performs abstraction selectively. This allows for compositionality and simpler yet accurate abstraction than abstract interpretation. The algorithm is optimized between the abstraction points using a proof summarization technique. The formal foundations include modeling of programs and high-level specifications in CLP, assertions to specify traditional safety which includes recursive data structure properties, as well as structural properties (e.g., symmetry), and a proof method and techniques for proving the assertions. Our framework handles traditional safety proof, data structure verification which precision is helped by selective abstraction, and reductions using symmetry or other structural properties which can handle more cases than existing approaches. We discuss implementations of variants of our general algorithm in CLP(R) and provide their running results.
URI: http://scholarbank.nus.edu.sg/handle/10635/13161
Appears in Collections:Ph.D Theses (Open)

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

OPEN

NoneView/Download

Page view(s)

247
checked on Dec 11, 2017

Download(s)

235
checked on Dec 11, 2017

Google ScholarTM

Check


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