Please use this identifier to cite or link to this item:
Title: A framework for program reasoning based on constraint traces
Keywords: program verification, program analysis, symbolic execution, abstraction, symmetry reduction, constraint logic programming
Issue Date: 23-May-2008
Citation: 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.
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



Google ScholarTM


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