Please use this identifier to cite or link to this item:
DC FieldValue
dc.titleA framework for program reasoning based on constraint traces
dc.contributor.authorANDREW EDWARD SANTOSA
dc.identifier.citationANDREW EDWARD SANTOSA (2008-05-23). A framework for program reasoning based on constraint traces. ScholarBank@NUS Repository.
dc.description.abstractWe 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.
dc.subjectprogram verification, program analysis, symbolic execution, abstraction, symmetry reduction, constraint logic programming
dc.contributor.departmentCOMPUTER SCIENCE
dc.contributor.supervisorJAFFAR, JOXAN
dc.description.degreeconferredDOCTOR OF PHILOSOPHY
Appears in Collections:Ph.D Theses (Open)

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



Page view(s)

checked on May 22, 2019


checked on May 22, 2019

Google ScholarTM


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